チャフアルゴリズム

Chaffは、プログラミングにおけるブール充足可能性問題を解くためのアルゴリズムです。プリンストン大学の研究者によって設計されました。このアルゴリズムは、効率的な実装のためにいくつかの改良が加えられたDPLLアルゴリズムの一種です。

このアルゴリズムのソフトウェア実装としては、mChaffと がありzChaff、後者が最も広く知られ、使用されています。zChaffは元々Lintao Zhang博士によって書かれたもので、そのため「z」が付けられています。現在はプリンストン大学の研究者によってメンテナンスされており、 Linux上でソースコードとバイナリの両方としてダウンロードできます。zChaffは非商用利用であれば無料です。

• M. Moskewicz、C. Madigan、Y. Zhao、L. Zhang、S. Malik。「Chaff: 効率的な SAT ソルバーの設計」、第 39 回設計自動化会議 (DAC 2001)、ラスベガス、ACM 2001。
• Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "ブール充足可能性ソルバーとそのモデル検査への応用". Proceedings of the IEEE . 103 (11): 2021–2035 . doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 . 

• zChaffに関するウェブページ