Local consistency and SAT-solvers

DOI10.1613/JAIR.3531zbMATH Open1237.68187arXiv1401.4613OpenAlexW2950058198WikidataQ129489138 ScholiaQ129489138MaRDI QIDQ2887073FDOQ2887073

Authors: P. Jeavons, J. Petke 

Publication date: 16 May 2012

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

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.

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

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

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)

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
• Graph-Theoretic Concepts in Computer Science
• Local consistency for extended CSPs
• Title not available (Why is that?)
• Representing and solving finite-domain constraint problems using systems of polynomials
• Local-search techniques for propositional logic extended with cardinality constraints
• Constraint Satisfaction Problems Solvable by Local Consistency Methods
• On the Power of k-Consistency

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)