FROM XSAT TO SAT BY EXHIBITING BOOLEAN FUNCTIONS

摘要

Given a Boolean formula in conjunctive normal form (CNF), the Exact Satisfiability problem (XSAT), a variant of the Satisfiability problem (SAT), consists in finding an assignment to the variables such that each clause contains exactly one satisfied literal. Best algorithms to solve this problem run in O(2~(0.2325n)) (O(2~(0.1379n)) for X3SAT). Another possibility is to transform each clause in a set of equivalent clauses for the Satisfiability problem and to use modern and powerful solvers (zChaff, Berkmin, MiniSat, RSat etc.) to find such truth assignment. In this paper we introduce three new encodings from XSAT instances to SAT instances that lead to a lot of structural information (equivalency gates and gates) which is naturally hidden in the pairwise transformation. Some solvers (lsat, march_dl, eqsatz) can take into account this kinds of structural information to make simplifications as pretreatment and speed-up the resolution. Then we show the interest of dealing with the XSAT formalism by introducing an encoding of binary CSP and graph coloring problem into XSAT instances. Preliminary results on real-world binary CSP and graph coloring problem show the importance of exhibiting equivalencies for the XSAT problem.