logic - 一次論理を CNF に変換する

Question

MiniSatを使用して制約充足問題を解決しようとしています。一次論理では、問題はいくつかの離散ドメイン変数といくつかの述語によって簡単に表されます。

しかし、MiniSat は、これまで見てきた他の CSP ソルバーと同様に、すべて CNF 形式での入力を必要とします。そこで、一次論理式を CNF に変換する一種の「プリプロセッサ」を探しています。

何かご意見は？

Answer 1

ベルギーのルーベンにあるカトリエケ大学の IDP3 を検討してみてください: http://dtai.cs.kuleuven.be/krr/software/idp3 ) ミニサットを適用します。

もう 1 つのオプションは、Koen Claessen (Chalmers U、スウェーデン) の Paradox です。Paradox は一次論理の有限モデル ファインダーであり、これも SAT への変換から始まり、MiniSAT を使用して式を解きます。Paradox のソース コードは、 http: //www.cse.chalmers.se/~koen/code/ からダウンロードできます。