TitleInference Rules for High-Order Consistency in Weighted CSP
Publication TypeConference Paper
Year of Publication2007
AuthorsAnsótegui C, Bonet MLuisa, Levy J, Manyà F
Conference NameProc. of the 22th AAAI Conference on Artificial Intelligence, AAAI-07
PublisherAAAI Press
Conference LocationVancouver, Canada

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.