Coupling different integer encodings for SAT

DOI10.1007/978-3-031-08011-1_5zbMath1502.68268OpenAlexW4285263050MaRDI QIDQ2170178

Peter J. Stuckey, Hendrik Bierlee, Graeme Gange, Jip J. Dekker, Guido Tack

Publication date: 30 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-08011-1_5

Mathematics Subject Classification ID

Boolean programming (90C09) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Uses Software

• MiniZinc
• Sugar
• Open-WBO
• Proteus
• PBLib
• Picat-SAT
• CHUFFED

Cites Work

• Compiling finite linear CSP into SAT
• PySAT: a Python toolkit for prototyping with SAT oracles
• Core-guided and core-boosted search for CP
• Propagation via lazy clause generation
• On CNF Encodings of Decision Diagrams
• A New Look at BDDs for Pseudo-Boolean Constraints
• Open-WBO: A Modular MaxSAT Solver,
• PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• Boolean Equi-propagation for Concise and Efficient SAT Encodings of Combinatorial Problems
• A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints
• Recent Advances in Constraints

This page was built for publication: Coupling different integer encodings for SAT