java - 如何将 boolean 表达式转换为cnf文件?

标签 java boolean-expression conjunctive-normal-form sat-solvers

<分区>

我需要使用 sat 求解器来检查 boolean 表达式的可满足性..

我有这样复杂的 boolean 表达式

alt text

是否有任何自动 cnf 文件转换器,以便我可以直接将其提供给 sat 求解器?

我读了cnf格式文件..但是如何在.cnf文件中表达这个表达式呢?当括号内有连词以及如何表达 --> 和 <-> 时,我感到困惑?请帮助我

最佳答案

有几个解决方案。

Limboole是一个开源工具,我相信它包括一个单独的“CNF 的命题逻辑”转换器。

更一般地说,您还可以使用原生支持命题逻辑的工具;一些示例包括 Z3 , CVC3 , 和 Yices .

关于java - 如何将 boolean 表达式转换为cnf文件?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/3948061/

相关文章:

java - 练习绘制一个星号正方形,星号之间有线条

java - 满足条件时增加map值

java - <s :if> test expression evaluation for boolean value doesn't work as expected

ruby - 在 Ruby 中评估许多 bool 表达式,如 Array#join

c++ - 如何将命题逻辑树转换为合取范式 (CNF) 树

computer-science - 3-cnf-sat有一个问题

expression - 将表达式转换为带有扭曲的合取范式

java - 在 JFrame 上隐藏 LoadingImage 或 LoadingPanel

java - 在@RequestParam 中绑定(bind)一个列表

sql - PostgreSQL 是否会短路其 BOOL_OR() 评估?