optimization - CNF 简化

Question

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

Answer 1

您可以使用 Norbert Manthey 的Riss3g 协处理器来简化您的CNF.

SAT求解器minisat 2允许将预处理CNF的数据存储在文件中。

SAT来自奥地利的求解器Lingeling"-s"可以选择简化CNF子句。

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