algorithm - DPLL 什么是一致的文字集？

Question

我正在编写 SAT 求解器，并开始实现 DPLL 算法。我了解该算法及其工作原理，我还实现了它的一个变体，但让我困扰的是接下来的事情。

function DPLL(Φ)
   if Φ is a consistent set of literals
       then return true;
   if Φ contains an empty clause
       then return false;
   for every unit clause l in Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

Φ 是一组一致的文字是什么意思？我理解inconsistent implies false，意思是consistent implies not false。那么，如果当前赋值没有伪造问题，为什么我们可以返回 true？

我实现 SAT 求解器的方式是，每当它遇到使所有子句都为真的赋值时，我返回该赋值并完成算法。但是由于对于给定的赋值，所有子句都必须为真才能解决问题，我不明白，如果赋值只是满足问题(我假设我在这里弄错了，但是因为如果 Φ 是一致的，那么这意味着它不是假的，但它仍然是不可判定的？)。

Answer 1

当仅包含文字和一个文字且其否定未出现在 Φ 中时，Φ 是一组一致的文字。 DPLL算法通过pure和unit规则，逐渐将子句列表转换为满足所有原始子句的文字列表。当这种情况发生时(Φ 是一组一致的文字)或当它用完要尝试的文字分配并且最顶层的 DPLL 调用返回 false 时，算法就会完成。