CNF 简化

Question

给定一组子句，我想首先检查它们是否可满足。如果是，我想简化它们并创建一个 CNF，例如，(a OR b) ^ (NOT b) 应该简化为：a ^ (NOT b)。我只使用命题公式。我尝试使用 Java SAT4j 库来执行此操作。它可以告诉我这组子句是否可以满足，但似乎没有任何方法可以让我返回一个简化的 CNF。我可以做些什么来有效地简化 CNF？是否有任何 Java 或 Python 实现？

Answer 1

您可以使用 Norbert Manthey 的 Riss3g Coprocessor 来简化您的 CNF。

SAT 求解器 minisat 2 允许 store the preprocessed CNF in a file。

Lingeling，来自奥地利的SAT 求解器有一个选项"-s" 来简化CNF 子句。

要将布尔表达式转换为简化的CNF，您可以使用bc2cnf。