Title :
New logical and complexity results for Signed-SAT
Author :
Ansótegui, Carlos ; Manyà, Felip
Abstract :
We define Mv-formulas as the union of the subclasses of signed CNF formulas known as regular and monosigned CNF formulas, and then define resolution calculi that are refutation complete for Mv-formulas and give new complexity results for the Horn-SAT and 2-SAT problems. Our goal is to use Mv-formulas as a constraint programming language between CSP and SAT, and solve computationally difficult combinatorial problems with efficient satisfiability solvers for Mv-formulas. The results presented in this paper provide evidence that Mv-formulas are a problem modeling language that offers a good compromise between complexity and expressive power.
Keywords :
Horn clauses; combinatorial mathematics; computability; computational complexity; constraint handling; decidability; problem solving; theorem proving; CSP; Horn-SAT; Mv-formulas; complexity results; computationally difficult combinatorial problems; constraint programming language; logical results; monosigned CNF formulas; problem modeling language; regular CNF formulas; resolution calculi; satisfiability solvers; signed-SAT; Artificial intelligence; Computer languages; Computer science; Encoding; Hardware; Multivalued logic; NP-complete problem; Polynomials;
Conference_Titel :
Multiple-Valued Logic, 2003. Proceedings. 33rd International Symposium on
Print_ISBN :
0-7695-1918-0
DOI :
10.1109/ISMVL.2003.1201404
