チャフアルゴリズム

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

ソフトウェアにおけるアルゴリズムの利用可能な実装としては、mChaffとがありzChaff、後者が最も広く知られ、使用されています。zChaff は、現在Microsoft Researchに所属^{する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). 「ブール充足可能性ソルバーとモデル検査におけるその応用」。IEEE論文集。103 (11): 2021–2035。doi : 10.1109 /JPROC.2015.2455034。S2CID 10190144  。

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