我正在努力使用MiniSat来解决约束满足问题。在一阶逻辑中，问题很容易用一些离散域变量和一些谓词来表示。
但是，MiniSat 以及我迄今为止看到的其他 CSP 求解器都希望他们以 CNF 形式输入。所以我正在寻找一种“预处理器”，它将一阶逻辑表达式转换为 CNF。
有什么想法吗？
问问题
5214 次
1 回答
3
您可能想考虑来自比利时鲁汶的 Katholieke Univ 的 IDP3：http: //dtai.cs.kuleuven.be/krr/software/idp3 IDP3 命题化一阶理论（具有归纳定义、聚合、有界算术的类型化一阶逻辑) 并应用 minisat。
另一种选择是来自 Koen Claessen（查默斯大学，瑞典）的 Paradox。Paradox 是一阶逻辑的有限模型查找器，它也从转换为 SAT 开始，然后使用 MiniSAT 求解公式。Paradox 的源代码可以从http://www.cse.chalmers.se/~koen/code/下载
于 2012-03-26T19:06:54.793 回答