research
∙
06/01/2023
Enumerating Disjoint Partial Models without Blocking Clauses
A basic algorithm for enumerating disjoint propositional models (disjoin...
share
research
∙
08/02/2022
Stratified Certification for k-Induction
Our recently proposed certification framework for bit-level k-induction-...
research
∙
07/27/2022
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
We give a first account of our new parallel SAT solver Gimsatul. Its key...
research
∙
10/22/2021
On Enumerating Short Projected Models
Propositional model enumeration, or All-SAT, is the task to record all m...
research
∙
05/09/2018
Revisiting Decision Diagrams for SAT
Symbolic variants of clause distribution using decision diagrams to elim...
research
∙
02/18/2014
Concurrent Cube-and-Conquer
Recent work introduced the cube-and-conquer technique to solve hard SAT ...
research
∙
11/23/2010