證明命題重言式的策略？

Question

輸入是一個帶有（任何）檢查語法的符號串，輸出爲TRUE或FALSE。

我的想法是用AND，XOR和TRUE編寫的邏輯表達式的修復後表示，但我終於意識到這些模式在修復後很難識別。

實例：

p蘊含q可以寫成TRUE XOR P（XOR（p和q））縮寫1個+ P + PQ

帶Q p等效可以寫縮寫1 + p + q

非p縮寫1 + p

p或q簡稱P + Q + PQ

在此布爾環的規則是相同的普通代數，與兩個規則

• 的p + p = 0時
• pp = p

並且這些規則與換向一起負責所有的縮減，如果字符串對應於重言式，則這將導致'1'。同義反復肯定前件，

（（對蘊含q）和p）蘊含q，

首先應如上述被取代，然後通過分佈式乘以擴展，和最後反覆被簡化。意味着一種直接替代給出：

1+((1+f+fg)f)+((1+f+fg)f)g = 
= 1+ f+ff+fgf +(f+ff+fgf)g = 
= 1+ f+f+fg + fg+fg+fg = 
= 1+ fg +fg+fg+fg = 1 

當同義反復表達在布爾環寫成的元件它減少機械爲1其它表達式簡化爲一個代數簡單的表達式。

這是一個很好的策略嗎？計算機科學使用什麼策略？

Answer 1

如本overview paper討論的，任意的命題公式可以以這樣一種方式，它僅具有多項式更大的尺寸和是不可滿足當且僅當原來的公式是同義反復被轉換成合取範式（CNF）。

從公式轉換爲CNF的實用工具包括bool2cnf和bc2cnf。

SAT solvers用於檢查CNF的不可滿足性包括CryptoMiniSat和Lingeling。

查看related post，其中顯示瞭如何使用SAT解算器處理命題公式。