Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint
From MaRDI portal
Publication:2398511
DOI10.1007/S10601-015-9232-8zbMATH Open1409.68266OpenAlexW2249204130MaRDI QIDQ2398511FDOQ2398511
Authors: Milan Banković 
Publication date: 16 August 2017
Published in: Constraints (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10601-015-9232-8
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
- Solving constraint satisfaction problems with SAT modulo theories
- meSAT: multiple encodings of CSP to SAT
- Maximal Flow Through a Network
- Handbook of constraint programming.
- Depth-First Search and Linear Graph Algorithms
- Propagation via lazy clause generation
- A machine program for theorem-proving
- Computer Aided Verification
- Title not available (Why is that?)
- Challenges in Satisfiability Modulo Theories
- Compiling finite linear CSP into SAT
- Principles and Practice of Constraint Programming – CP 2004
- Generalised arc consistency for the AllDifferent constraint: an empirical survey
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Tools and Algorithms for the Construction and Analysis of Systems
- Lazy clause generation: combining the power of SAT and CP (and MIP?) solving
- URBiVA: uniform reduction to bit-vector arithmetic
Cited In (1)
Uses Software
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)
