3

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

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

替代文字

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

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

4

2 回答 2

6

有几个解决方案。

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

更一般地说,您还可以使用原生支持命题逻辑的工具;一些例子包括Z3​​ 、CVC3Yices

于 2011-01-17T19:58:14.013 回答
2

SBSAT是一个基于状态的 SAT 求解器,能够接受多种输入格式。您可以取一个简单的表达式并将其提供给 SBSAT 以转换为 CNF。手册第4.10 节介绍了如何执行此操作。

于 2012-11-06T03:09:29.330 回答