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 and 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}
    • 同样，单位传播是适用的，但现在会导致空公式，这是可以满足的。

使用单元子句 (UC) 或纯字面量 (PL) 中的哪一个来解决这个具体示例？

单元子句传播用于解决此示例。并且由于公式的对称性，选择不同顺序的拆分文字将导致相同的结果。