当使用MiniSat作为C++库时，每个新变量都可以创建为决策变量或非决策变量。
我对此的粗略理解是，当求解器决定在分支期间下一步使用哪个变量时，不考虑非决策变量。然而，在我的项目中，当非决策变量位于暗示的左侧而不是等价关系时，我遇到了麻烦，因为求解器返回 SAT，即使公式实际上是 UNSAT。
进一步的实验表明，只有当非决策变量位于长度超过 2 个变量的公式中时，才会发生这种情况（我猜 2 变量公式路径是求解器中的一个特例，因此它的行为不同）。
非决策变量只能通过推理来设置其值。 Minisat使用的唯一推理方法是单位规则。 因此，如果设置所有决策变量不会导致调用单位规则来设置所有非决策变量，则永远不会设置后一个变量。
使用非决策变量的通常原因是，您知道 CNF 实例的结构使得设置一组固定的决策变量将暗示所有其他变量的值。
这方面的一个例子是 CNF 实例，用于查找某个 n 位整数的素因数。 该实例必须实现实现乘法的移位加法器电路链，但您只需要设置作为乘法电路输入的 2（n-1） 位。 表示这些位的变量将是决策变量，所有其他变量都可以安全地声明为非决策变量。