sat - MiniSat 中非决策变量的语义是什么？

Question

当使用 MiniSat 作为 C++ 库时，每个新变量都可以创建为决策变量或非决策变量。

我对此的粗略理解是，当求解器在分支期间决定接下来使用哪个变量时，不考虑非决策变量。然而，在我的项目中，当非决策变量位于蕴涵的左侧而不是处于等价关系时，我遇到了麻烦，因为求解器返回 SAT，即使公式实际上是 UNSAT。

进一步的实验表明，这仅在非决策变量位于长于 2 个变量的公式中时才会发生(我猜 2 变量公式路径在求解器中是一种特殊情况，因此它的行为不同)。

Answer 1

非决策变量只能通过推理设置它们的值。 Minisat 使用的唯一推理方法是单位规则。因此，如果设置所有决策变量不会导致调用单元规则来设置所有非决策变量，则永远不会设置后者变量。

具有非决策变量的通常原因是您知道 CNF 实例的结构使得设置一组固定的决策变量将暗示所有其他变量的值。

这方面的一个例子是 CNF 实例，用于查找一些 n 位整数的质因数。该实例必须实现一系列实现乘法的移位加法器电路，但您只需要设置作为乘法电路输入的 2(n-1) 位。代表这些位的变量将是决策变量，所有其他变量都可以安全地声明为非决策变量。