meSAT: multiple encodings of CSP to SAT

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

zbMATH Keywords

CSPSATalgorithm portfolioencoding CSP to SAT

Mathematics Subject Classification ID

Mixed integer programming (90C11) Nonlinear programming (90C30)

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

• MiniSat
• Paramils
• MiniZinc
• SATzilla
• URBiVA
• Sugar
• Azucar
• BEE

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