Boolean Satisfiability Research Group at Princeton

zChaff

NEW: zChaff 2007.3.12 is available both in 32 bit version and 64 bit version. It fixes the inefficiency bug in zverify_df. Thanks to Allen Van Gelder and Tjark Weber for reporting the bug and proving the fixes.

zChaff 2004.11.15 is available here. It is a trimmed version of 2004.5.13. Many unused or dead codes are removed. Most codes are re-formatted for easy reading. You might get a little speed up as well. If the functionality that you require is removed, please use the original 2004.5.13 version below.

The source for zChaff 2004.5.13 is available for download here.

We request you to read the copyright notice before downloading the software. For commercial licensing, please contact Princeton University.

The description file for SAT04 explains What's New

Old version (2001.2.17) is available Here.

zChaff is an implementation of the Chaff algorithm. This solver is now maintained (occasionally) by Yogesh Mahajan. zChaff is designed with performance and capacity in mind. We have success stories of using zChaff to solve problems with more than one million variables and 10 million clauses. (Of course, it can't solve every such problem!).

zChaff has been tested on Solaris/Linux/Cygwin machines with g++ as the compiler. It can be compiled with Visual Studio .Net under Windows.

zChaff can be compiled into a linkable library for integration purpose so that the users do not need to export instances into intermediate files to use zChaff. See zChaff in action at SAT-Ex . Successful integration examples include AI Planner BlackBox , Model Checker NuSMV , Theorem Prover GrAnDe .