DPLL和可滿足性示例？

Question

我們知道DPLL算法是回溯+單位傳播+純文字規則。

我舉個例子。用DPLL解決以下可滿足性問題有一個例子。如果將變量「0」賦值給變量之前，將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）被用來解決這個具體的例子？

單位子句傳播用於解決這個例子。由於公式的對稱性，選擇不同順序的分割文字將導致相同的結果。