我正在努力使用MiniSat解决约束满足问题。在一阶逻辑中，问题很容易由几个离散域变量和一些谓词表示。
但是，MiniSat以及到目前为止我所见过的其他CSP求解器，都希望它们以CNF形式输入。因此，我正在寻找一种可以将一阶逻辑表达式转换为CNF的“预处理器”。
有什么想法吗？
最佳答案
您可能想考虑来自比利时鲁汶的Katholieke大学的IDP3:http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3命题化一阶理论(带有归纳定义，聚合，有界算术的类型化一阶逻辑)并应用minisat。
另一种选择是来自Koen Claessen(瑞典，卡尔默斯大学)的悖论。 Paradox是一阶逻辑的有限模型查找器，它也首先转换为SAT，然后使用MiniSAT求解公式。可以从http://www.cse.chalmers.se/~koen/code/下载Paradox的源代码