BooleForce and TraceCheck

Overview

BooleForce is a SAT solver similar to MiniSAT. As unique feature it keeps proof traces in memory and thus can generate variable and clausal cores in memory as well. Compared to zChaff and MiniSAT this speeds up core generation dramatically. However, memory may become a bottle neck for very large proofs.

TraceCheck

The BooleForce distribution also contains the source code of our resolution trace checker TraceCheck. In the file README.tracecheck you find an overview and a description of the format accepted by TraceCheck. TraceCheck has been succesfully used for regression testing of a couple of SAT solvers. It also was essential in the context of our BDD based SAT solver EBDDRES. You may find more information on the previous home page of TraceCheck.

Download

[ booleforce-1.3.tar.gz | booleforce-1.2.tar.gz | booleforce-1.1.tar.gz | booleforce-1.0.tar.gz ]

Version 1.3 adds a new option but otherwise is just a maintenance release.

Version 1.2 fixes some minor compilation issues on 64-bit machines and Darwin.

The second public release of BooleForce mainly provided new features for TraceCheck. In NEWS you find a list of new features. The README contains more information on compilation and installation.

License

We use a BSD style license. In essence, you can use and modify the sources as you like provided that you acknowledge the origin of the software. More details can be found in the LICENSE file that comes with the sources.