Satisfiability: Theory, Practice, and Beyond 2023
2023-04-17..2023-04-20
Berkeley, United States
who it's for
satisfiability researchers, SAT solver developers, constraint programming researchers, MaxSAT developers, QBF researchers, formal methods engineers, knowledge compilation researchers
topics
CDCL conflict-driven learning; IPASIR user propagators; MaxSAT proof logging; QBF proof systems; sum-of-squares certificates; stabbing planes proofs; cutting planes simulations; certified symmetry breaking; sampler testing and Barbarik; Conjure abstract modelling; MCSat for nonlinear arithmetic; knowledge compilation for synthesis
| title | author | length |
|---|---|---|
| In Search of the Hard Instances | Albert Atserias | 01h 16m |
Partial survey that ties concrete lower/upper bounds, sum-of-squares algebraic proofs, and proof-search hardness to practical SAT behavior. Shows the… | ||
| A Survey of Automatability | Robert Robere | 01h 05m |
Defines automatability as finding a proof within time bounded by the shortest proof length and contrasts algorithms and lower bounds. Gives the trivial 2^s… | ||
| On Bounded Depth Proofs For Tseitin Formulas On The Grid; Revisited | Kilian Risse | 30m |
Proves that bounded-depth Frege refutations of the Tseitin formula on an n × n torus require length exp( n / (log M)^O(d) ) when every line has size ≤ M and… | ||
| CDCL SAT Solving and Applications to Optimization Problems | Alexander Nadel | 01h 01m |
Concise primer on CDCL specifics (GRASP vs Chaff, two-watched literals, BCP internals, first-UIP clause conflict extraction and the tradeoff between… | ||
| IPASIR-UP: User Propagators for CDCL | Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere | 31m |
Proposes a minimal standardized extension to IPASIR called IPASIR-UP interface that exposes four notifications and five callbacks to inspect and influence CDCL… | ||
| Designing Samplers is Easy: The Boon of Testers | Kuldeep S. Meel | 31m |
A scalable grey-box tester called Barbarik tester uses conditional sampling to distinguish samplers without needing samples proportional to the solution count… | ||
| Structure-guided Local Improvement for Maximum Satisfiability | André Schidler | 25m |
Presents a method that iteratively extracts tiny subinstances by growing a frontier from unsatisfied soft clauses on the primal graph expansion, fixes the rest… | ||
| A Roadmap for the Next Phase of SAT Research | Karem Sakallah | 01h 10m |
Argues CDCL’s power comes from combining conflict-driven learning with conflict-driven branching, conjectures that many human-created CNF encodings have… | ||
| Beyond SAT - Proofs for QBF, and more | Meena Mahajan | 48m |
Overview of what is known and what still fails: four concrete QBF proof paradigms — expansion, universal reduction — plus literal merging/long‑distance… | ||
| The Proof Complexity of Integer Programming | Noah Fleming | 59m |
Introduces Stabbing Planes as a proof system modeling branch-and-cut and proves a constructive translation that, when each query has bounded-coefficient… | ||
| Theoretical limits of 1UIP Learning | Marc Vinyals | 33m |
Shows explicit CNF families with linear-length resolution proofs but that force CDCL with 1UIP (or any reasonable learning) to incur a quadratic blowup in… | ||
| Clique is hard on average for unary Sherali-Adams | Susanna F. de Rezende | 35m |
Claim: for G~G(n,1/2) with high probability, unary Sherali‑Adams needs size n^{Omega(log n)} to refute the existence of a k‑clique even when k = n^{Omega(1)}… | ||
| Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz | Shuo Pang | 29m |
Proves that polynomial calculus and Nullstellensatz require linear degree (hence a strongly exponential-size lower bound) to refute that sparse random… | ||
| Isomorph-Free Generation Of Combinatorial Objects With Sat Modulo Symmetries | Stefan Szeider, Katalin Fazekas, Markus Kirchweger, Tomas Peitl, Manfred Scheucher | 47m |
SMS claims a practical, certifying way to generate combinatorial objects without isomorphic duplicates by integrating a CDCL SAT solver with dynamic… | ||
| Logic, Optimization, and Constraint Programming: A Fruitful Collaboration | John Hooker | 01h 02m |
Asserts concrete equivalences and tools: conflict clauses are Benders cuts — SAT/SMT conflict learning is derivable from inference duality — and resolution… | ||
| ASP: Theory, Practice, and Beyond | Torsten Schaub | 42m |
Answer Set Programming is a rule‑based modeling language with a grounding+solving pipeline (Gringo→Clingo) that enforces stable model semantics via the logic… | ||
| Modern Constraint Programming, For People Who Know SAT | Ciaran McCreesh | 50m |
Overview of modern constraint programming versus SAT with concrete differences: model languages like MiniZinc and Essence, stateful propagators, and lazy… | ||
| Rado numbers: SAT methods and connections to Nullstellensatz complexity | William J. Wesley | 38m |
Computations produce hundreds of new exact Rado numbers and a SAT method that generates SAT-based formulas for three infinite families of three‑color Rado… | ||
| Exact Covering with Colours | Don Knuth | 24m |
Defines exact covering with color (XCC) that generalizes exact cover and CSPs, adds just a few dozen lines to an existing solver, and implements both dancing… | ||
| Benefits of Abstract Modelling using Conjure | Özgür Akgün | 48m |
A toolchain centered on Conjure + Essence takes a high-level, typed problem specification and automatically generates many low-level encodings via Essence… | ||
| Exploiting Combinatorial Structure in Constraint Programming: ... | Gilles Pesant | 47m |
Shows how constraint programming yields exact and approximate counts (19 solutions and 10/19 marginals in a regular constraint DAG example), gives a practical… | ||
| The Power of Extended Resolution: A Practitioner's Perspective | Randal Bryant | 01h 05m |
Extended resolution is used to attach concise, checkable proofs to non‑CDCL reasoning: a BDD‑based proof generator emits DRAT/LRAT clauses so Gaussian… | ||
| Reactive Synthesis Empowered by Logical Reasoning | Rayna Dimitrova | 45m |
Overview of SAT-based reactive synthesis with concrete encodings and results: bounded synthesis searches for finite-state implementations up to a given size… | ||
| MCSat Approaches for Solving Non-linear Modular Arithmetic | Daniela Kaufmann | 47m |
Presents two concrete MCSat-based solvers: PolySAT in Z3, a word-level bitvector solver that keeps variable domains as symbolic intervals, extracts forbidden… | ||
| Trustworthy Automated Reasoning | Marijn Heule | 01h 03m |
Claims validated with formally-verified proof checker: Boolean Pythagorean Triples is unsatisfiable for 1..7,824 with proofs that reach terabytes to petabytes… | ||
| Certified Static and Dynamic Symmetry Breaking | Bart Bogaerts | 31m |
This work shows how to produce machine-verifiable certificates for both static symmetry breaking and a prototype of dynamic symmetry breaking by encoding… | ||
| Proof Logging for MaxSAT – The Past, The Present and The Future | Jeremias Berg | 28m |
MaxSAT is effective but lacks mature proof logging; recent work uses SAT solvers plus pseudo-Boolean cutting planes and finds real bugs where solvers perform… | ||
| Proof Logging for Constraint Programming | Matthew McIlree | 30m |
A pseudo-Boolean proof system, VeriPB, records backtracking search by emitting negations of decision sequences as RUP steps and extends with cutting-planes to… | ||
| Homomorphism Counts: Expressive Power and Query Algorithms | Phokion Kolaitis | 01h 05m |
Lovász’s theorem and its database analogue anchor a view where left profile and right profile are vectors of homomorphism counts; Dvořák shows Ck-equivalence… | ||
| Analysis of Core-Guided MaxSat Using Cores and Correction Sets | Nina Narodytska | 47m |
Proves that core-guided MaxSAT and hitting-set solvers recover the same original-core structure and that the minimum hitting set equals optimum when computed… | ||
| Proving UNSAT in Zero Knowledge | Ning Luo | 48m |
A practical zero‑knowledge protocol proves propositional UNSAT by encoding clauses as polynomials and checking resolution steps as algebraic relations over a… | ||
| Knowledge Compilation for Quantification and Synthesis | Supratik Chakraborty | 01h 04m |
Claims that a much weaker compiled form than OBDDs/DNNFs suffices to do existential quantification and Boolean functional synthesis in polytime: the synthesis… | ||
| Explaining SAT Solving Using Causal Reasoning | Jiong Yang | 32m |
CausalSAT runs solvers on UNSAT benchmarks, logs clause features and uses DRAT-trim to count clause utility (uses in the proof over the next 10,000 conflicts)… | ||
| Unification of SAT, Constraint Programming, and Pseudo-Boolean Solving: A Personal Story | Emir Demirovic | 33m |
Argues SAT CP and pseudo-Boolean solvers are essentially the same at a conceptual level and gives concrete transfers: clause learning → lazy clause generation… | ||
| SAT Beyond Boolean Interpretations | Vinodchandran Variyam | 18m |
Given a CNF formula, the goal is to maximize its value under interpretations over a semiring K rather than Boolean truth; for the Viterbi semiring (values in… | ||
| nothing matches | ||