产生无法满足的测试问题

我正在尝试为命题可满足性生成一些测试问题，特别是生成一些无法满足的问题，但是根据固定的模式，以便对于任何N，都可以生成N个变量的无法满足的问题。

一个简单的解决方案是x1，x1=>x2，x2=>x3 ... !xN，除了这是所有SAT求解器都可以立即处理的单位子句之外，因此那不是一个足够艰难的测试。

N个变量无法满足的问题的模式是什么，这些变量不是随机的，通过检查可以看出是不能满足的，但对于SAT求解器至少是不平凡的？

Pigeonhole problems是non-trivial，适用于未经预处理的基于CDCL的SAT求解器，即参见Detecting Cardinality Constraints in CNF。论文Hard Examples for Resolution可能会让您感兴趣。

想到的第一个示例是对包含每个变量的所有可能的析取取并一次。例如，如果您的变量是p1，p2和p3：

（¬p1∨p2∨p3）∧（¬p1∨p2∨p3）∧（¬p1∨p2¬p3）∧（¬p1∨p2∨p3）∧（p1∨p2∨¬ p3）∧（p1∨¬p2∨p3）∧（p1∨p2¬¬p3）∧（p1∨p2∨p3）

另一种描述方式是：对所有可能赋值的求和。例如，¬（p1∧p2∧p3）=（¬p1∨p2∨p3）是公式的子句。因此，每个可能的赋值都不能完全满足一个子句。但是，我们只知道这一点，因为我们验证了这些条款的穷举性。

如果我们尝试转换为规范的析取范式，则无论我们按什么顺序尝试变量，我们都无法更快地完成，最终得到：

（p1∧¬p1∧p2∧p3）∨（p1∧p2¬¬p2∧p3）∨（p1∧p2∧p3∧p3）

我们生成的每个子句在哪里都不令人满意，但是只有当我们扩展所有子句时，我们才会看到这一点。如果我们尝试寻找令人满意的分配，无论我们按什么顺序尝试变量，我们都只能在指数时间内详尽地测试每个可能的分配。

可能会有一个SAT求解器对此特殊情况进行测试，尽管测试每个可能的子句都在输入中本身会花费指数时间，并且将任意输入放入规范形式中，您可以有效地说出，只是三个变量的八个可能子句，我们已经检查了是否有重复项，也需要一段时间。