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

我需要使用解算器坐了检查布尔表达式的可满足..如何将布尔表达式转换为cnf文件？

我有复杂的布尔表达式这样

alt text

有任何自动CNF文件转换器，这样我可以直接给它坐解决者？

我读取cnf格式文件..但如何在.cnf文件中表达这个表达式？当palenthesis中存在连词时，我会感到困惑，并且如何表达 - >和< - >？请帮我

来源

2010-10-16 karthi

有几个解决方案。

Limboole是一个开放源代码的工具，我相信它包括一个单独的'CNF'转换器的命题逻辑。

更一般地说，你也可以使用一种本机支持命题逻辑的工具;一些示例包括Z3,CVC3和Yices。

来源

2011-01-17 19:58:14 phooji

您所命名的SMT解算器真的可以解决SAT解决问题的难题.... – EfForEffort 2012-11-06 03:06:52

@DenisBueno：我很同意（SMT求解器比SAT解决方案做得更多）。在这种情况下，我并没有真正看到成本 - 现代基于DPLL（T）的SMT解算器具有与最好的仅SAT解算器相媲美的SAT性能，而且使用起来也不那么困难。如果你愿意使用SMT-lib语法，你可以编写相当高层次的命题，并且仍然可以互换使用解算器。我会补充一点，Z3，cvc3和yices正在积极维护并且有相当活跃的邮件列表来支持用户。 – phooji 2012-11-06 04:13:02

SBSAT是一种基于状态的SAT求解器，能够接受各种输入格式。你可以采取一个简单的表达式，并将其提供给SBSAT以转换为CNF。 manual，第4.10节描述了如何做到这一点。

来源

2012-11-06 03:09:29 EfForEffort

我无法在'SBSAT'中找到这样的功能。可以将“跟踪格式”指定为输入格式。但是，这不允许嵌套的布尔表达式，但只允许门语句的网表。 – 2014-01-16 13:17:15

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

回答

相关问题