Sciweavers

AAAI
2007

Inference Rules for High-Order Consistency in Weighted CSP

13 years 6 months ago
Inference Rules for High-Order Consistency in Weighted CSP
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,...
Carlos Ansótegui, Maria Luisa Bonet, Jordi
Added 02 Oct 2010
Updated 02 Oct 2010
Type Conference
Year 2007
Where AAAI
Authors Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy, Felip Manyà
Comments (0)