Proceedings 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2000) (2000)

Portland, Oregon

May 23, 2000 to May 25, 2000

ISSN: 0195-623X

ISBN: 0-7695-0692-5

pp: 331

Bernhard Beckert , University of Karlsruhe

Reiner Hähnle , Chalmers University of Technology

Felip Manyà , University of Lleida

ABSTRACT

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 this paper we present 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.

INDEX TERMS

Many-valued logic, signed logic, NP-completeness, SAT

CITATION

B. Beckert, F. Manyà and R. Hähnle, "The 2-SAT Problem of Regular Signed CNF Formulas,"

*Proceedings 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2000)(ISMVL)*, Portland, Oregon, 2000, pp. 331.

doi:10.1109/ISMVL.2000.848640

CITATIONS