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

DOI10.1007/S10817-010-9204-ZzbMATH Open1243.68264OpenAlexW1985449294MaRDI QIDQ438582FDOQ438582

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

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

zbMATH Keywords

resolution methodproof systemSAT/CSP encoding

Mathematics Subject Classification ID

Cites Work

• Theory and Applications of Satisfiability Testing
• BerkMin: A fast and robust SAT-solver
• Theory and Applications of Satisfiability Testing
• Generalized Arc Consistency for Positive Table Constraints
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• Networks of constraints: Fundamental properties and applications to picture processing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Random constraint satisfaction: Flaws and structure
• On forward checking for non-binary constraint satisfaction.
• A Generalized Framework for Conflict Analysis
• On the parallel complexity of discrete relaxation in constraint satisfaction networks
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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

Uses Software

• MiniSat
• CSPLib
• Chaff

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)