问DPLL和满足性示例？

EN

下面是如何使用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)是用来解决这个具体的例子？

使用单位子句传播来解决这个例子。由于公式的对称性，选择不同顺序的分裂字会得到相同的结果。