New Insights into Encodings from MaxCSP into Partial MaxSAT
Modelling Max-CSP as Partial Max-SAT
Publication Type:
Conference PaperSource:
11th International Conference on Theory and Applications of Satisfiability Testing (SAT-2008), Springer, Volume 4996, Guangzhou, China, p.1-14 (2008)Keywords:
Max-SAT; Max-CSPAbstract:
We define a number of original encodings that map Max-CSP instances
into partial Max-SAT instances. Our encodings rely on the well-known
direct and support encodings from CSP into SAT. Then, we report on an
experimental investigation that was conducted to compare the
performance profile of our encodings on random binary Max-CSP
instances. Moreover, we define a new variant of the support encoding
from CSP into SAT which produces fewer clauses than the standard
support encoding.
Inference Rules for High-Order Consistency in Weighted CSP
Publication Type:
Conference PaperSource:
Proc. of the 22th AAAI Conference on Artificial Intelligence, AAAI-07, AAAI Press, Vancouver, Canada, p.167-172 (2007)Keywords:
CSPAbstract:
Recently defined resolution calculi for Max-SAT and signed Max-SAT have provided a logical characterization of the solving techniques applied by Max-SAT and WCSP solvers. In this paper we first define a new resolution rule, called signed Max-SAT parallel resolution, and prove that it is sound and complete for signed Max-SAT. Second, we define a restriction and a generalization of the previous rule called, respectively, signed Max-SAT i-consistency resolution and signed Max-SAT (i,j)-consistency resolution. These rules have the following property: if a WCSP signed encoding is closed under signed Max-SAT i-consistency, then the WCSP is i-consistent, and if it is closed under signed Max-SAT (i,j)-consistency, then the WCSP is (i,j)-consistent. A new and practical insight derived from the definition of these new rules is that algorithms for enforcing high order consistency should incorporate an efficient and effective component for detecting minimal unsatisfiable cores. Finally, we describe an algorithm that applies directional soft consistency with the previous rules.
