logic - 将一阶逻辑转换为 CNF

Question

我正在努力使用 MiniSat解决约束满足问题。在一阶逻辑中，问题很容易由几个离散域变量和一些谓词表示。

但是，MiniSat 以及我目前看到的其他 CSP 求解器都希望以 CNF 形式输入。因此，我正在寻找一种可以将一阶逻辑表达式转换为 CNF 的“预处理器”。

有什么想法吗？

Answer 1

您可能会考虑来自比利时鲁汶 Katholieke 大学的 IDP3:http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3 propositionalises 一阶理论(带归纳定义、聚合、有界算术的类型化一阶逻辑)并应用 minisat。

另一个选择是来自 Koen Claessen(瑞典查默斯大学)的 Paradox。 Paradox 是一阶逻辑的有限模型查找器，它也从转换为 SAT 开始，然后使用 MiniSAT 求解公式。 Paradox 的源代码可以从http://www.cse.chalmers.se/~koen/code/ 下载。