将一阶逻辑转换为 CNF
我正在努力使用 MiniSat 来解决约束满足问题。在一阶逻辑中，问题很容易用一些离散域变量和一些谓词来表示。
然而，MiniSat 以及我迄今为止见过的其他 CSP 求解器都希望以 CNF 形式输入。所以我正在寻找一种“预处理器”，它将一阶逻辑表达式转换为 CNF。
有什么想法吗？
I'm endeavouring to use MiniSat to solve a constraint satisfaction problem. In first-order logic the problem is easily represented by a few discrete-domain variables and some predicates.
However, MiniSat, along with the other CSP solvers I've seen so far, would all like their input in CNF form. So I'm in search of a "preprocessor" of sorts which will convert first-order logic expressions into CNF.
Any thoughts?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您可能会考虑比利时鲁汶天主教大学的 IDP3：http://dtai.cs .kuleuven.be/krr/software/idp3 IDP3 命题化一阶理论（具有归纳定义、聚合、有界算术的类型化一阶逻辑）并应用小型卫星。
另一种选择是 Koen Claessen（瑞典查尔姆斯大学）的 Paradox。 Paradox 是一个用于一阶逻辑的有限模型查找器，它也是从转换为 SAT 开始，然后使用 MiniSAT 求解公式。 Paradox 的源代码可以从 http://www.cse.chalmers.se/ 下载~koen/代码/
You might like to consider IDP3 from Katholieke Univ of Leuven, Belgium: http://dtai.cs.kuleuven.be/krr/software/idp3 IDP3 propositionalises first-order theories (typed first order logic with inductive definitions, aggregates, bounded arithmetic) and applies minisat.
Another option would be Paradox from Koen Claessen (Chalmers U, Sweden). Paradox is a finite model finder for first order logic, that also starts by translating to SAT and then solves the formula using MiniSAT. The source code of Paradox can be downloaded from http://www.cse.chalmers.se/~koen/code/