International Symposium on Multiple-valued Logic, 1999
Bernhard Beckert, Reiner Haehnle, Felip Manya
Signed conjunctive normal form (signed CNF) is a classical conjunctive
clause form using a generalized notion of literal, called signed atom. A
signed atom 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".
Applications for deduction in signed logics derive from those of
annotated logic programming (e.g., mediated deductive databases),
constraint programming (e.g., scheduling), and many-valued logics (e.g.,
natural language processing). The central role of signed CNF justifies
a detailed study of its subclasses, including algorithms for and
complexities of associated SAT problems.
In continuation of our work presented at ISMVL'99, we present in this
paper new results on the complexity of the signed 2-SAT problem; i.e.,
the case in which all clauses of a signed CNF formula have at most two
literals.