我正在尝试生成一些命题可满足性的测试问题，特别是生成一些不可满足的问题，但是根据固定模式，这样对于任何 N，都可以生成 N 个变量的不可满足问题。
一个简单的解决方案是x1, x1=>x2, x2=>x3...!xN除了这将是所有单元子句，任何 SAT 求解器都可以立即处理，所以这不是一个足够艰难的测试。
N 个变量的不可满足问题的模式是什么，这些变量不是随机的并且可以通过检查看出是不可满足的，但对于 SAT 求解器来说至少有些不重要？
问问题
126 次
2 回答
3
对于没有预处理的基于 CDCL 的 SAT 求解器，鸽巢问题是不平凡的，即参见Detecting Cardinality Constraints in CNF。您可能会对解决问题的硬性示例一文感兴趣。
于 2020-09-28T09:41:24.443 回答
1
想到的第一个例子是对包含每个变量的所有可能析取进行一次合取。例如，如果您的变量是 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 求解器来测试这种特殊情况，尽管测试输入中的每个可能的子句本身会花费指数时间，并且将任意输入放入规范形式中，您可以有效地说，只有八个三个变量的可能子句，我们已经检查过没有重复，也需要一段时间。
于 2020-09-27T23:47:02.930 回答