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可以用来解决示例公式的方法：

• 由于没有unit子句，因此无法传播 unit。
• 纯文字规则不适用，因为不存在仅正面或负面出现的文字。
• 要应用拆分规则，请选择一些文字，例如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）用于解决此特定示例？

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