Chaff is an

algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing ...

for solving instances of the

Boolean satisfiability problem In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfie ...

in programming. It was designed by researchers at

Princeton University Princeton University is a private research university in Princeton, New Jersey. Founded in 1746 in Elizabeth as the College of New Jersey, Princeton is the fourth-oldest institution of higher education in the United States and one of the ...

. The algorithm is an instance of the

DPLL algorithm In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solvi ...

with a number of enhancements for efficient implementation.

Implementations

Some available implementations of the algorithm in software are mChaff and zChaff, the latter one being the most widely known and used. zChaff was originally written by Dr. Lintao Zhang, at Microsoft Research, hence the “z”. It is now maintained by researchers at

and available for

download In computer networks, download means to ''receive'' data from a remote system, typically a server such as a web server, an FTP server, an email server, or other similar system. This contrasts with uploading, where data is ''sent to'' a remote ...

as both source code and binaries on

Linux Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, w ...

. zChaff is free for non-commercial use.

References

* M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik.
Chaff: Engineering an Efficient SAT Solver
', 39th Design Automation Conference (DAC 2001), Las Vegas, ACM 2001. *

External links

SAT solvers Boolean algebra Automated theorem proving Constraint programming {{formalmethods-stub