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

Question

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

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

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

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

Answer 1

有几个解决方案。

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

更一般地说，您还可以使用原生支持命题逻辑的工具；一些例子包括Z3​​ 、CVC3和Yices。

Answer 2

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