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

当使用MiniSat作为C++库时，每个新变量都可以创建为决策变量或非决策变量。MiniSat中的非决策变量的语义是什么？

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

进一步的实验表明，只有当非决策变量在一个长于2个变量的公式中时才会出现这种情况（我认为2变量公式路径是解算器中的一种特殊情况，因此它的行为有所不同）。

来源

2017-10-13 Xarn

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

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

一个这样的例子是一个CNF实例来找到一些n位置整数的主要因素。该实例必须实现一系列实现乘法的移位加法器电路，但您只需设置输入到乘法电路的位即可。表示这些位的变量将是决策变量，所有其他变量可以安全地声明为非决策变量。

来源

2017-10-13 21:29:05

这对于CNF的可满足性意味着什么？即将所有变量标记为决策变量，我可以说CNF是SAT，如果每个子句至少有一个文字评估为真。我的简短实验表明，对于具有非决策变量的CNF，CNF被报告为SAT，如果每个决策变量被设置为true或false，并且每个子句都具有评估为true的文字，或者undef。真的吗？ – Xarn

如果所有决策变量都已成功赋值，Minisat会报告SAT。它不关心其他事情。如果Minisat无法为所有决策变量分配值，则报告UNSAT，因为单位规则的应用在变量耗尽之前总是产生冲突。通过冲突我的意思是说，一个变量需要既是真实的又是假的，以满足由于当前任务而失去单位的条款。 –

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

回答

相关问题