java - ブール式をcnfファイルに変換するには?

Question

ブール式の充足可能性をチェックするために sat ソルバーを使用する必要があります..

このような複雑なブール式があります

satソルバーに直接渡すことができる自動cnfファイルコンバーターはありますか?

cnf形式のファイルを読んだのですが、この式を.cnfファイルでどのように表現すればよいのでしょうか? 括弧内に接続詞があると混乱し、 --> と <-> をどのように表現するか? 私を助けてください

Answer 1

いくつかの解決策があります。

Limbooleはオープンソースツールであり、別の「命題論理からCNFへ」のコンバーターが含まれていると思います。

より一般的には、命題論理をネイティブにサポートするツールを使用することもできます。いくつかの例には、Z3、CVC3、およびYicesが含まれます。

Answer 2

SBSATは、さまざまな入力形式を受け入れることができる状態ベースの SAT ソルバーです。単純な式を SBSAT に渡して CNF に変換することができます。マニュアルのセクション 4.10 に、これを行う方法が説明されています。