Solving constraint satisfaction problems with SAT modulo theories

DOI10.1007/S10601-012-9123-1zbMATH Open1309.90099OpenAlexW2015135969WikidataQ57979695 ScholiaQ57979695MaRDI QIDQ487632FDOQ487632

Authors Miquel Bofill, Miquel Palahí, Josep Suy, Mateu Villaret 

Publication date 22 January 2015

Published in Constraints (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10601-012-9123-1

zbMATH Keywords

constraint programmingsatisfiability modulo theoriesreformulationsolvers and tools

Mathematics Subject Classification ID

Nonlinear programming (90C30) Boolean programming (90C09)

Recommendations

• On SAT Modulo Theories and Optimization Problems
• Constraint programming for modelling and solving modal satisfiability
• Satisfiability modulo theories and assignments
• Satisfiability modulo theories
• Applying modern SAT-solvers to solving hard problems
• Modal Satisfiability via SMT Solving

Cites Work

• scientific article; zbMATH DE number 2080324 (Why is no real title available?)
• scientific article; zbMATH DE number 1903342 (Why is no real title available?)
• A system for solving constraint satisfaction problems with SMT
• Challenges in Satisfiability Modulo Theories
• Compiling finite linear CSP into SAT
• Constraint Logic Programming Using ECLⁱPS^e
• Deciding Combinations of Theories
• Efficient theory combination via Boolean search
• Essence: A constraint language for specifying combinatorial problems
• From Propositional Satisfiability to Satisfiability Modulo Theories
• Lazy satisfiability modulo theories
• On SAT Modulo Theories and Optimization Problems
• Philosophy of the MiniZinc challenge
• Propagation via lazy clause generation
• Satisfiability modulo the theory of costs: foundations and applications
• Simplification by Cooperating Decision Procedures
• Solvable cases of the decision problem
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in $\mathit{SMT}(\mathcal{EUF} \cup \mathcal{T})$

Cited In (17)

• Set constraint model and automated encoding into SAT: application to the social golfer problem
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Inferring Congruence Equations Using SAT
• Solving Difficult SAT Problems by Using OBDDs and Greedy Clique Decomposition
• Multi-agent pathfinding with continuous time
• Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences
• Solving String Theories Involving Regular Membership Predicates Using SAT
• SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
• SAT-solving in CSP trace refinement
• Solving the resolution-free SAT problem by submodel propagation in linear time
• fzn2smt
• Train scheduling with hybrid answer set programming
• Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
• Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
• SAT Modulo Differential Equation Simulations
• A system for solving constraint satisfaction problems with SMT
• Constraint solving for finite model finding in SMT solvers

Uses Software

• SCIP
• SMT-LIB
• Yices
• z3
• MiniZinc
• FlatZinc
• Gecode
• JaCoP
• MathSAT
• Sugar
• SIMPLY
• SICStus
• Essence

This page was built for publication: Solving constraint satisfaction problems with SAT modulo theories

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