Local consistency and SAT-solvers

DOI10.1613/JAIR.3531MaRDI QIDQ2887073zbMATH OpenOpenAlexWikidataFDO

Authors P. Jeavons, J. Petke

Publication date 16 May 2012

Published in The Journal of Artificial Intelligence Research (JAIR) (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.4613

zbMATH Keywords

SATconstraint satisfaction problemsproblem solvinglocal consistency\(k\)-consistencyclause-learning SAT-solvers

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: Local consistency techniques such as k-consistency are a key component of specialised solvers for constraint satisfaction problems. In this paper we show that the power of using k-consistency techniques on a constraint satisfaction problem is precisely captured by using a particular inference rule, which we call negative-hyper-resolution, on the standard direct encoding of the problem into Boolean clauses. We also show that current clause-learning SAT-solvers will discover in expected polynomial time any inconsistency that can be deduced from a given set of clauses using negative-hyper-resolvents of a fixed size. We combine these two results to show that, without being explicitly designed to do so, current clause-learning SAT-solvers efficiently simulate k-consistency techniques, for all fixed values of k. We then give some experimental results to show that this feature allows clause-learning SAT-solvers to efficiently solve certain families of constraint problems which are challenging for conventional constraint-programming solvers.

Recommendations

• Theory and Applications of Satisfiability Testing
• On the power of clause-learning SAT solvers as resolution engines
• scientific article; zbMATH DE number 2243370
• Local consistency for extended CSPs
• Local Consistency in Weighted CSPs and Inference in Max-SAT

Cited in

(10)

• Theory and Applications of Satisfiability Testing
• Tractability in constraint satisfaction problems: a survey
• The Power of Local Consistency in Conjunctive Queries and Constraint Satisfaction Problems
• Local consistency for extended CSPs
• Graph-Theoretic Concepts in Computer Science
• scientific article; zbMATH DE number 5996383 (Why is no real title available?)
• Representing and solving finite-domain constraint problems using systems of polynomials
• Constraint Satisfaction Problems Solvable by Local Consistency Methods
• Local-search techniques for propositional logic extended with cardinality constraints
• On the Power of k-Consistency

Describes a project that uses

Uses Software

• MiniZinc

This page was built for publication: Local consistency and SAT-solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2887073)