我们知道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）编写。为什么选择其中两个？任何的想法？