logo标签列表

如何将布尔表达式转换为 CNF 文件？

javaboolean-expressionconjunctive-normal-formsat-solvers
3
我需要使用SAT求解器来检查布尔表达式的可满足性。
我有一个像这样的复杂布尔表达式：
（图片被省略）
是否有自动CNF文件转换器，以便我可以直接将其输入给SAT求解器？
我已经阅读了CNF格式文件，但如何在.cnf文件中表示这个表达式呢？当括号内有合取时，我感到困惑。还有，如何表示-->和<->？请帮帮我。
2个回答
6
有几种解决方案。 Limboole 是一个开源工具，我相信其中包括一个独立的“命题逻辑到CNF”的转换器。
更一般地，您还可以使用支持命题逻辑本地化的工具；一些例子包括Z3、CVC3和Yices。
你提到的SMT求解器对于SAT求解来说确实有些过头了... - EfForEffort
@DenisBueno：我有点同意（SMT求解器做的事情不仅仅是SAT求解）。但在这种情况下，我并没有真正看到成本——现代基于DPLL(T)的SMT求解器具有与最佳SAT-only求解器相当的SAT性能，并且它们使用起来并不那么困难。如果你愿意使用SMT-lib语法，你可以编写相当高级的命题内容，并且仍然可以交替使用求解器。我还要补充的是，Z3、cvc3和yices正在积极维护，并拥有相当活跃的邮件列表来支持用户。 - phooji
2

SBSAT是一种基于状态的SAT求解器，能够接受各种输入格式。您可以将简单的表达式交给SBSAT来转换为CNF。该手册第4.10节描述了如何操作。

我在 SBSAT 中找不到这样的功能。可以将“跟踪格式”指定为输入格式。但是，这不允许嵌套布尔表达式，而只允许门语句的网表。 - Axel Kemper
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接