Chaff is an algorithm for solving instances of the Boolean satisfiability problem, designed by researchers at Princeton University. It is an instance of the DPLL algorithm with a number of enhancements aimed at an efficient implementation. It was described in the paper Chaff: Engineering an Efficient SAT Solver by Moskewicz, Madigan, Zhao, Zhang and Malik, presented at the 39th Design Automation Conference in Las Vegas in 2001, and it is discussed again in a 2015 survey of Boolean satisfiability solvers and their applications in model checking. Two software implementations are named, mChaff and zChaff. zChaff is the most widely known and used, and it takes the z from its original author, Dr. Lintao Zhang. It is now maintained by researchers at Princeton University and is available as source code and as Linux binaries, free for non-commercial use.
Connections
In Field
Source Chaff algorithm (Wikipedia)
Sources
Chaff algorithm (Wikipedia)
In Group: Logic and Foundations, Lead
The algorithm is an instance of the DPLL algorithm with a number of enhancements for efficient implementation.
In Field: Theory of Computation, Lead, satisfiability
Chaff is an algorithm for solving instances of the Boolean satisfiability problem in programming.
View the SourceReader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.