meSAT: multiple encodings of CSP to SAT
From MaRDI portal
Publication:2342599
DOI10.1007/s10601-014-9165-7zbMath1316.90049OpenAlexW2012978749MaRDI QIDQ2342599
Mirko Stojadinović, Filip Marić
Publication date: 29 April 2015
Published in: Constraints (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10601-014-9165-7
Related Items (7)
Portfolio theorem proving and prover runtime prediction for geometry ⋮ \textsc{Conjure}: automatic generation of constraint models from problem specifications ⋮ Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint ⋮ Learning to select SAT encodings for pseudo-Boolean and linear Integer constraints ⋮ Why CP Portfolio Solvers Are (under)Utilized? Issues and Challenges ⋮ meSAT ⋮ Wombit: a portfolio bit-vector solver using word-level propagation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Compiling finite linear CSP into SAT
- Propagation via lazy clause generation
- A Boolean satisfiability approach to the resource-constrained project scheduling problem
- Compiling problem specifications into SAT
- Another look at graph coloring via propositional satisfiability
- NP-SPEC: an executable specification language for solving all problems in NP
- Perfect Hashing and CNF Encodings of Cardinality Constraints
- Pairwise Cardinality Networks
- URSA: A System for Uniform Reduction to SAT
- The Log-Support Encoding of CSP into SAT
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Cardinality Networks and Their Applications
- ParamILS: An Automatic Algorithm Configuration Framework
- Compiling finite domain constraints to SAT withBEE
- An Empirical Evaluation of Portfolios Approaches for Solving CSPs
- Statistical Methodology for Comparison of SAT Solvers
- A System for Solving Constraint Satisfaction Problems with SMT
- Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers
- Theory and Applications of Satisfiability Testing
- URBiVA: Uniform Reduction to Bit-Vector Arithmetic
This page was built for publication: meSAT: multiple encodings of CSP to SAT