CNF简化

Question

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

Answer 1

您可以使用诺伯特庄园的Riss3g 协处理器来简化您的CNF。

SAT解决程序迷你型2允许使用在文件中。

来自奥地利的凌岭是SAT的一个求解者，它有一个简化CNF子句的选项"-s"。

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