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));

Φ是一组一致的文字，这意味着什么？我理解不一致意味着错误，这意味着

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

Answer 1

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