1

我正在编写一个 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));

这是什么意思，这Φ是一组一致的文字？我理解不一致意味着假，这意味着一致意味着不假。true那么，如果当前的分配没有证伪问题，为什么我们可以返回呢？

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

4

1 回答 1

2

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

于 2017-11-02T17:22:28.277 回答