Python SAT with pycosat

Question

我有一个类赋值，其中我需要编写一个使用pycosat库测试SAT的函数。我很难找出一组从库中返回"UNSAT“的参数。有没有人能帮我找出一组“不可解”的参数？查看该库的单元测试，我能找到的唯一实例是[1，-1]

**作业要复杂得多，我只想了解用于测试我的作业的SAT求解器。

Answer 1

回答我自己的问题:你需要创造一个矛盾。创建3个变量(A、B、C)。为了创建一个无法求解的计算，您需要创建一个使其无法求解的布尔操作。

(A或B)和(不是A或B)和(B或C)和(不是B或C)

真值表将表明，A、B或C的值的任何组合都不会导致上述计算为真。为了表示pycosat，它将如下所示：

[1，2，-1，-2，2，3，-2，3]