Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
From MaRDI portal
Publication:2398511
Recommendations
- Solving finite-domain linear constraints in presence of the $\texttt{alldifferent}$
- A system for solving constraint satisfaction problems with SMT
- Constraint solving for finite model finding in SMT solvers
- Interleaved Alldifferent Constraints: CSP vs. SAT Approaches
- Natural domain SMT: a preliminary assessment
Cites work
- scientific article; zbMATH DE number 3338381 (Why is no real title available?)
- A machine program for theorem-proving
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Challenges in Satisfiability Modulo Theories
- Compiling finite linear CSP into SAT
- Computer Aided Verification
- Depth-First Search and Linear Graph Algorithms
- Generalised arc consistency for the AllDifferent constraint: an empirical survey
- Handbook of constraint programming.
- Lazy clause generation: combining the power of SAT and CP (and MIP?) solving
- Maximal Flow Through a Network
- Principles and Practice of Constraint Programming – CP 2004
- Propagation via lazy clause generation
- Solving constraint satisfaction problems with SAT modulo theories
- Tools and Algorithms for the Construction and Analysis of Systems
- URBiVA: uniform reduction to bit-vector arithmetic
- meSAT: multiple encodings of CSP to SAT
This page was built for publication: Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2398511)
