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

Question

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

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

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

Answer 1

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

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

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