下载。
我正在尝试使用MiniSat来解决约束满足问题。在一阶逻辑中，这个问题很容易用几个离散域变量和一些谓词来表示。
然而，MiniSat以及我迄今为止看到的其他CSP求解器都希望它们的输入是CNF形式。因此，我正在寻找一种"预处理器"，它将一阶逻辑表达式转换为CNF。
任何想法吗?
你可能想考虑来自比利时鲁汶大学的IDP3: http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3命题化一阶理论(带归纳定义、聚合、有界算术的类型化一阶逻辑)并应用miniat。
另一个选择是来自Koen Claessen (Chalmers U, Sweden)的Paradox。Paradox是一阶逻辑的有限模型查找器，它也从转换为SAT开始，然后使用MiniSAT解决公式。Paradox的源代码可以从http://www.cse.chalmers.se/~koen/code/