Navigation: Front Page Proof Format Overview Publications
VeriPB lets you trust that algorithms are giving the correct answer.
VeriPB is a general-purpose proof format for certificates of correctness produced by proof-logging algorithms. The underlying proof system uses pseudo-Boolean reasoning: cutting planes on 0-1 integer linear inequalities, augmented with strengthening and convenience rules. It can express and certify a range of sophisticated combinatorial solving techniques. Documentation of the format as used in the 2025 SAT competition is available here.
A number of combinatorial solvers can produce VeriPB proofs, including:
| The BreakID SAT symmetry breaker |
The CaDiCaL SAT solver | The CGSS MaxSAT solver |
| The Exact pseudo-Boolean solver |
The Glasgow Constraint Solver | The Glasgow Subgraph Solver |
| The Pacose MaxSAT solver |
The PaPILO MIP pre-solver |
The QMaxSATpb MaxSAT solver |
| The RoundingSat pseudo-Boolean solver |
The satsuma SAT symmetry breaker |
The Scuttle multi-objective MaxSAT solver |
Researchers working on VeriPB and associated projects have benefitted from support and hosting from many organisations, including:
A series of tutorials on VeriPB proof logging and its applications was given at WHOOPS '25
