New logical and complexity results for Signed-SAT

Author

Ansótegui, Carlos ; Manyà, Felip

fYear

2003

fDate

16-19 May 2003

Firstpage

181

Lastpage

187

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Multiple-Valued Logic, 2003. Proceedings. 33rd International Symposium on

ISSN

0195-623X

Print_ISBN

0-7695-1918-0

Type

conf

DOI

10.1109/ISMVL.2003.1201404

Filename

1201404