Labelled Deduction
Bernhard Beckert, Reiner H\"ahnle, Felip Manya
The SAT Problem of Signed CNF Formulas
Abstract:
Signed conjunctive normal form (signed CNF) is a classical conjunctive
clause form using a generalised notion of literal, called signed
literal. A signed literal is an expression of the form S:p, where p is a
classical atom and S, its sign, is a subset of a domain N. The informal
meaning is "p takes one of the values in S". Signed formulas are a
logical language for knowledge representation that lies in the
intersection of the areas constraint programming (CP), many-valued logic
(MVL), and annotated logic programming (ALP). This central role of
signed CNF justifies a detailed study of its subclasses including
algorithms for and complexities of associated satisfiability problems
(SAT problems). Although signed logic is used since the 1960s, there are
only few systematic investigations of its properties. In contrast to
work done in ALP and MVL, our present work is a more fine-grained study
for the case of propositional CNF. We highlight the most interesting
lines of current research: (i) signed versions of some main proponents
of classical deduction systems including non-trivial refinements having
no classical counterpart; (ii) incomplete local search methods for
satisfiability checking of signed formulas; (iii) phase transition
phenomena as known, for example, from classical SAT and the influence of
the cardinality of N on the crossover point; (iv) the complexity of the
SAT problem for signed CNF and its subclasses.