了解DPLL算法

Question

我想了解 DPLL算法 解决SAT问题。在这里是：

Algorithm DPLL
  Input: A set of clauses Φ.
  Output: A Truth Value.
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));

起初，我不清楚地了解 unit-propagate(l, Φ), pure-literal-assign(l, Φ) 和 choose-literal(Φ) 工作。我将尝试猜测特定的例子。请纠正我，如果我做错了什么。

• 对于第一个

  unit-propagate(a, (0 v -a) ∧ (a v b) ∧ (b v d) ∧ (f v g) v ...)

  我们将有

  ((0 v -0) ∧ (0 or 1) ∧ (1 v d) ∧ (f v g) ∧ ... = (f v g) v ...,

  有 a = 0, b = 1.

• 用于第二个过程

  pure-literal-assign(a, (a v b v c) ∧ (d v -b v a) ∧ (-d v b))

  结果是

  (b v c) ∧ (d v -b) ∧ (-d v b),

  分配 a = 1.

• 最后 choose-literal(Φ) 只是返回一些随机（常见）未分配的文字进行进一步计算。

现在，我不明白为什么算法有如此奇怪的条件来完成？为什么起作用？

谢谢！

Answer 1

之所以起作用，是因为您提到的三种情况将在一定的步骤后删除每个非伪变量，但是至关重要的是，您也考虑递归步骤，即$ mbox {dpll}（ phi phi land l） lor mbox {dpll}（ phi land neg l）$。

递归步骤后，您保证至少具有一个单位子句，因此单位子句将设置为其值，因此所有变量最终都将分配一个值。

我认为您的误解必须来自递归电话。观察，如果您有任何公式$ phi =（（（a lor b lor c） land cdots）$，则$ mbox {select-literal}（ phi）$将返回一些未分配的变量，例如$。然后，递归电话将带有$ phi land a $，将为$（a lor b lor c） land cdots） land（a）$。然后$ mbox {unit-literal}（ phi）$将返回$ a $并将其设置为true。另一个递归电话是等效的，但是使用$ phi land（ neg a）$，因此$ mbox {unit-literal}（ phi）$仍然会返回$ a $ a $并将$ a $设置为false。

Answer 2

我认为您的问题不是算法本身，而是周围的一些概念。

1. 一个 文字 是变量或否定的：例如，$ a $或$ neg a $。
2. 一个 条款 是文字的脱节：$ a lor b $
3. 一个 单位子句 仅包含一个文字：$ neg a $就是一个例子
4. 这 空句 不包含文字，并写成$ {} $或$（）$或$ box $。空子句无法满足，您可以将其视为等同于$ false $。
5. 一个 联合正常形式（CNF） 公式是条款的结合：$（a lor b） land（ neg a）$
6. 这 空的公式 不包含条款，并编写$ emptyset $。每个作业都可以满足空的公式，您可以将其视为$ true $。

请注意一个空句和空公式之间的区别。这些是算法操纵的基本对象。现在我们来运营。

1. 这 单位规则 说，如果我们有一个单位条款$ neg a $和条款$ a lor theta $，那么为了满足公式，我们必须满足条款$ theta $。这是因为要满足单位条款$ neg a $，必须将变量$ a $设置为$ false $含义，我们无法满足$ a $，因此我们必须满足$ theta $。单位传播反复应用单位规则。
2. 观察到，在执行上述单位规则时，我们正在从条款中删除不满意的文字，而只留下可能有助于满足该条款的文字。如果我们删除所有文字，我们将拥有空的子句，这意味着该子句的限制是无法满足的，进而意味着整个公式无法满足。
3. 这 纯粹的文字规则 是基于这样的观察结果：如果一个变量仅在整个公式中发生一个极性，这意味着我们要么只有$ a $ a $，要么只有$ neg a $ a $ a $ a $，那么永远不会有任何限制公式中的$ a land（ neg a lor b）$。因此，我们可以使这个字面上的真实。这将满足其字面意思发生的每个条款，因此我们可以删除这些整个条款。

单位传播和纯粹的文字规则之间存在差异。单位传播从一个子句中删除文字，并使我们更接近发现是否存在空句，在这种情况下，公式无法满足。纯文字规则删除了整个条款，并使我们更接近空的公式，在这种情况下，公式在很大程度上令人满意。

如果您考虑上述两个案例，则发现它不能涵盖所有可能的行为。具体来说，可能没有任何单位条款，也可能没有任何纯文字。在这种情况下，为了取得进步，我们选择了单位子句中不出现并为其分配值的字面意义。可以将选择文字步骤视为将单元子句添加到公式中，该公式具有触发更多单位传播的效果。