雙變量邏輯可滿足性的新解法與實作分析

Abstract

我們重新審視了不具有相等謂詞之雙變量邏輯的可滿足性問題，以 SAT(FO2) 表示。這個問題已知是 NEXP-完全。 在本學位論文中，我們引入了一個圖論問題，命名為「條件性獨立集（CIS）」。我們提出了針對 CIS 的兩個演算法：一個時間複雜度為 O(1.4423^n) 的確定性演算法和一個時間複雜度為 O(1.6181^n) 的隨機性演算法，其中 n 是圖系統當中的謂詞數量。我們也提出了 SAT(FO2) 至 CIS 的歸約，並得到相當的兩個針對 SAT(FO2) 的演算法：一個時間複雜度為 O(1.4423^(2^n)) 的確定性演算法和一個時間複雜度為 O(1.6181^(2^n)) 的隨機性演算法，其中 n 是 Scott's 正規型態式子中的謂詞數量。 我們提供了 SAT(FO2) 求解器的實作細節，包含將 FO2 式子轉換為 Scott's 正規型態、將 SAT(FO2) 歸約至 CIS 和解決 CIS。 我們針對九種類的輸入式子進行了相關的實驗。在實驗中，我們比較了我們實作的求解器與另外兩種求解器的效率。我們也測量了我們的求解器在各階段的執行時間，以此來分析我們的求解器的強項與缺點。實驗結果顯示我們的演算法與實作應該是正確的，且它們的效率整體而言優於其他的求解器。