Boolean Satisfiability Research Group at Princeton

Software

Chaff The Chaff SAT solver is a state of the art Boolean Satisfiability Solver designed for robustness and efficiency. It features a highly optimized deduction engine and pioneered the VSIDS decision strategy.

In SAT 2004 Competition, our solver zChaff emerged as the Best Complete Solver in industrial benchmark category (and industrial unsatisfiable benchmarks category). It was also awarded in SAT 2002 Competition as the Best Complete Solver in both industrial and handmade benchmarks categories.

Currently we have two distributions of the Chaff SAT Solver. [These solvers are provided as is without any warranty.]

mChaff

zChaff

Quaffle Quaffle is an experimental QBF solver that incorporate Conflict and Satisfaction Driven Learning and Backtracking. It is maintained by Yinlei Yu

Quaffle: Quantified Boolean Formula Evaluator with Learning

Please contact the authors of the respective solvers for particular solver related questions.