algorithm - DPLL 和可满足性示例？

Question

我们知道DPLL算法是回溯+单元传播+纯文字规则。

我有一个例子。有一个例子可以用 DPLL 解决以下可满足性问题。如果将“0”分配给变量先于将“1”分配给变量，则使用 Unit Clause (UC) 或 Pure Literal (PL) 中的哪一个来解决此问题具体例子？

{~A \/ B \/ C}, {A \/ ~B \/ C}, {A \/ B \/ ~C}, {A \/ B \/ C}

在本例中使用其中两个(PL 和 UC)编写。为什么选择其中两个？任何想法？

Answer 1

以下是如何使用 DPLL 来求解您的示例公式:

• 单位传播是不可能的，因为没有单位条款。
• 纯文字规则不适用，因为没有仅出现在正面或仅出现在负面的文字。
• 要应用拆分规则，请选择一些文字，例如A。
  • 设置A=0 并传播。这将导致
    {1\/B\/C}, {0\/~B\/C}, {0\/B\/~C}, {0\/B\/C}
    == {~B\/C}, {B\/~C}, {B\/C}
  • 单位传播和纯文字仍然不适用。
  • 对下一个文字 B 应用拆分规则。
    • 设置B=0并传播:
      {1\/C}, {0\/~C}, {0\/C}
      == {~C}, {C}
    • 此公式由两个单元子句组成，因此可以应用单元传播，这会产生 {}，因此我们回溯。
    • 设置B=1 并传播。{0\/C}, {1\/~C}, {1\/C}
      == {C}
    • 同样，单位传播 是适用的，但现在会产生空公式，这很容易满足。

Which of Unit Clause (UC) or Pure Literal (PL) is used to solve this specific example?

Unit Clause propagation 用于解决这个例子。并且由于公式的对称性，选择不同顺序的拆分字面量会得到相同的结果。