Dealing with satisfiability and n-ary CSPs in a logical framework

DOI10.1007/S10817-010-9204-ZMaRDI QIDQ438582zbMATH OpenOpenAlexFDO

Authors Belaïd Benhamou, Lionel Paris, Pierre Siegel

Publication date 31 July 2012

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-010-9204-z

zbMATH Keywords

resolution methodproof systemSAT/CSP encoding

Mathematics Subject Classification ID

Recommendations

• A Boolean Encoding Including SAT and n-ary CSPs
• Mapping CSP into Many-Valued SAT
• The logic of constraint satisfaction
• Principles and Practice of Constraint Programming – CP 2003
• GAC Via Unit Propagation

Cites work

• scientific article; zbMATH DE number 4162321 (Why is no real title available?)
• scientific article; zbMATH DE number 3571520 (Why is no real title available?)
• scientific article; zbMATH DE number 2080318 (Why is no real title available?)
• scientific article; zbMATH DE number 1414299 (Why is no real title available?)
• scientific article; zbMATH DE number 1448978 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Generalized Framework for Conflict Analysis
• A Machine-Oriented Logic Based on the Resolution Principle
• BerkMin: A fast and robust SAT-solver
• Generalized Arc Consistency for Positive Table Constraints
• Networks of constraints: Fundamental properties and applications to picture processing
• On forward checking for non-binary constraint satisfaction.
• On the parallel complexity of discrete relaxation in constraint satisfaction networks
• Random constraint satisfaction: Flaws and structure
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(6)

• Satisfiability of acyclic and almost acyclic CNF formulas
• Satisfiability of acyclic and almost acyclic CNF formulas
• SAT-solving in CSP trace refinement
• CSP and Kripke Structures
• A Boolean Encoding Including SAT and n-ary CSPs
• Mapping CSP into Many-Valued SAT

Describes a project that uses

Uses Software

• Chaff
• CSPLib
• MiniSat

This page was built for publication: Dealing with satisfiability and \(n\)-ary CSPs in a logical framework

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