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

A novel approach to the satisfiability of two-variable logic and its practical analysis

林廷衛(Ting-Wei Lin)

指導教授 ： 陳偉松

國立臺灣大學/電機資訊學院/資訊工程學研究所/碩士(2021年)

https://doi.org/10.6342/NTU202102417

摘要

我們重新審視了不具有相等謂詞之雙變量邏輯的可滿足性問題，以 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。
我們針對九種類的輸入式子進行了相關的實驗。在實驗中，我們比較了我們實作的求解器與另外兩種求解器的效率。我們也測量了我們的求解器在各階段的執行時間，以此來分析我們的求解器的強項與缺點。實驗結果顯示我們的演算法與實作應該是正確的，且它們的效率整體而言優於其他的求解器。

關鍵字

雙變量邏輯 ； 可滿足性 ； 條件性獨立集

並列摘要

We revisit the satisfiability problem for two-variable first-order logic without equality, denoted by SAT(FO2). This problem is known to be NEXP-complete.
In this thesis we introduce a graph-theoretic problem that we call Conditional Independent Set (CIS). We present two algorithms to \cis: a deterministic algorithm with run time O(1.4423^n) and a randomized algorithm with run time O(1.6181^n), where n is the number of vertices in the graph system. Then we present reduction from SAT(FO2) to CIS, and yield the same two algorithms for SAT(FO2): a deterministic algorithm with run time O(1.4423^(2^n)) and a randomized algorithm with run time O(1.6181^(2^n)), where n is the number of predicates when the formula is in Scott normal form.
We provide the details of our implementation for the solver that decides SAT(FO2). This includes transforming FO2 formula into Scott normal form, reducing SAT(FO2) to CIS and deciding CIS.
We then perform experiments on 9 families of formulas. In the experiments, we compare the performance of our solver using different algorithms with two other solvers. We also measure the break-down of the run time of our solver to analyze its strengths and weaknesses. Experimental results show that our implementation of the algorithms seems correct and it is more efficient than other solvers in general.

並列關鍵字

two variable logic ； satisfiability ； conditional independent set

參考文獻

[1] Z3 solver, 2020. https://github.com/Z3Prover.

[2] C. Bron and J. Kerbosch. Finding all cliques of an undirected graph (algorithm 457). Commun. ACM, 16(9):575–576, 1973.

[3] A. Church. A note on the entscheidungsproblem. J. Symb. Log., 1(1):40–41, 1936.

[4] A. Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):pp. 345–363, 1936.

[5] M. Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, pages 312–319, 1983.