[  news | download | background ]

News

This is a tool to check propositional resolution proofs as generated for instance by SAT solvers. Our main usage is in regression testing of SAT solvers and therefore the whole proof can be assumed to fit into main memory. The goal was to have a simple input format, which is easy to produce and also easy to read for humans. This helps tremendously to debug incorrect proofs and buggy SAT solvers.

Download

TraceCheck became part of the source distribution of BooleForce.

Background

Beside being very important for testing purposes and debugging of SAT solvers, resolution proofs can be used for many other purposes, such as abstraction refinement through core generation, diagnosis of inconsistencies in product configuration and interpolation. References to these applications are given in our paper on using a BDD based SAT solver to produce extended resolution proofs for combinatorial hard problems.

Resolution and in particular extended resolution are the most powerful known proof systems. Since our proof checker can handle standard resolution, hyper resolution, extended resolution and in particular resolution chains produced by SAT solvers based on learning, the format is quite general. You find more information on the format in the README.

In the current version the solver does not distinguish between original clauses and clauses introduced through extended resolution. Therefore extended resolution proofs are only checked modulo the assumption that the variables introduced in extended resolutions steps are fresh and their definitions non cyclic. In a future release we want to lift this restriction by explicitly asking the user to provide a bound on the number of original variables. The tool can then check that the definitions introduce only new variables. Currently we are also working on a binary format and a more efficient implementation.