Unification of SAT, Constraint Programming, and Pseudo-Boolean Solving: A Personal Story
summary
Argues SAT CP and pseudo-Boolean solvers are essentially the same at a conceptual level and gives concrete transfers: clause learning → lazy clause generation and conflict analysis across paradigms, linear search (Sat4j) outperforming core‑guided MaxSAT on timetabling, and core‑guided search recast by introducing an integer variable for a core. Shows logic‑based Benders = implicit hitting sets, documents solution‑guided search becoming standard, and claims communities form around benchmarks so evaluation sets and engineering work often matter more than declared novelty.
AI-written summary · about
chapters (6)
- 0:00Introduction and motivation
- 1:15A unified view of paradigms
- 3:54Technique cross-pollination
- 5:34Structural insights and views
- 10:42Benchmarks and scientific impact
- 25:20Discussion and Q&A
related talks
01h 21mComputational Complexity in Theory and in Practice
01h 07mSatisfiability Algorithms I
17mSatisfiability Algorithms Based on Concentrated Shrinkage
21mMassive proofs for the masses
29mImproved Deterministic Algorithms for Sparse Max-SAT
58mCircuit Complexity and Connections I
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata
25mSymbolic Bisimulation for Open and Parameterized Systems