Chaff is an

algorithm In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...

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) asks whether there exists an Interpretation (logic), interpretation that Satisf ...

in programming. It was designed by researchers at

Princeton University Princeton University is a private university, private Ivy League research university in Princeton, New Jersey, United States. Founded in 1746 in Elizabeth, New Jersey, Elizabeth as the College of New Jersey, Princeton is the List of Colonial ...

. The algorithm is an instance of the DPLL algorithm 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 Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technologi ...

, 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 systems. This contrasts with uploading, where data is ''sent to'' a remote ...

as both source code and binaries on

Linux Linux ( ) is a family of open source Unix-like operating systems based on the Linux kernel, an kernel (operating system), operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically package manager, pac ...

. 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