http://debianws.lexgopc.com/wiki143/index.php?action=history&feed=atom&title=Chaff_algorithmChaff algorithm - Revision history2026-05-09T18:47:19ZRevision history for this page on the wikiMediaWiki 1.43.1http://debianws.lexgopc.com/wiki143/index.php?title=Chaff_algorithm&diff=1474700&oldid=previmported>Graeme Bartlett: mark software names2023-09-28T23:56:06Z<p>mark software names</p>
<p><b>New page</b></p><div>{{Short description|Programming algorithm}}{{no footnotes|date=July 2017}}<br />
'''Chaff''' is an [[algorithm]] for solving instances of the [[Boolean satisfiability problem]] in programming. It was designed by researchers at [[Princeton University]]. The algorithm is an instance of the [[DPLL algorithm]] with a number of enhancements for efficient implementation.<br />
<br />
== Implementations ==<br />
<br />
Some available implementations of the algorithm in software are <code>mChaff</code> and '''<code>zChaff</code>''', the latter one being the most widely known and used. zChaff was originally written by Dr. Lintao Zhang, {{clarify span|now|reason=Since when?|date=April 2019}} at [[Microsoft Research]], hence the “z”. It is now maintained by researchers at [[Princeton University]] and available for [[download]] as both source code and binaries on [[Linux]]. zChaff is free for non-commercial use.<br />
<br />
== References ==<br />
{{reflist}}<br />
* M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik. ''[http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf Chaff: Engineering an Efficient SAT Solver]'', 39th Design Automation Conference (DAC 2001), Las Vegas, ACM 2001.<br />
* {{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| pages = 2021–2035 | s2cid = 10190144 }}<br />
<br />
== External links ==<br />
* [http://www.princeton.edu/~chaff/zchaff.html Web page about zChaff]<br />
<br />
[[Category:SAT solvers]]<br />
[[Category:Boolean algebra]]<br />
[[Category:Automated theorem proving]]<br />
[[Category:Constraint programming]]<br />
<br />
<br />
{{formalmethods-stub}}</div>imported>Graeme Bartlett