請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/79765完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 陳偉松(Tony Tan) | |
| dc.contributor.author | Ting-Wei Lin | en |
| dc.contributor.author | 林廷衛 | zh_TW |
| dc.date.accessioned | 2022-11-23T09:10:22Z | - |
| dc.date.available | 2021-08-20 | |
| dc.date.available | 2022-11-23T09:10:22Z | - |
| dc.date.copyright | 2021-08-20 | |
| dc.date.issued | 2021 | |
| dc.date.submitted | 2021-08-17 | |
| dc.identifier.citation | [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. [6] E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two-variable firstorder logic. Bull. Symbolic Logic, 3(1):53–69, 03 1997. [7] E. Grädel and M. Otto. On logics with two variables. Theor. Comput. Sci., 224(1-2):73–113, 1999. [8] R. Graham, D. Knuth, and O. Patashnik. Concrete Mathematics: A Foundation for Computer Science, 2nd Ed. Addison-Wesley, 1994. [9] S. Itzhaky, T. Kotek, N. Rinetzky, M. Sagiv, O. Tamir, H. Veith, and F. Zuleger. On the automated verification of web applications with embedded SQL. In ICDT, pages 16:1–16:18, 2017. [10] A. Kahr, E. Moore, and H. Wang. Entscheidungsproblem reduced to the ∀∃∀ case. Proc. Nat. Acad. Sci. U.S.A., 48:365–377, 1962. [11] T. Kotek. FO2-Solver, 2017 (accessed April 10, 2020). https://forsyte.at/ alumni/kotek/fo2-solver/. [12] H. Lewis. Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci., 21(3):317–353, 1980. [13] T. Lin, C. Lu, and T. Tan. Towards a more efficient approach for the satisfiability of two-variable logic. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, 2021. [14] J. Moon and L. Moser. On cliques in graphs. Israel J. Math., 3:23–28, 1965. [15] M. Mortimer. On language with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21:135–140, 1975. [16] D. Scott. A decision method for validity of sentences in two variables. The Journal of Symbolic Logic, page 377, 1962. [17] E. Tomita, A. Tanaka, and H. Takahashi. The worst-case time complexity for generating all maximal cliques and computational experiments. Theor. Comput. Sci., 363(1):28–42, 2006. [18] B. Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. In D. Akad. Nauk USSR, 70(1), pages 569–572, 1950. [19] S. Tsukiyama, M. Ide, H. Ariyoshi, and I. Shirakawa. A new algorithm for generating all the maximal independent sets. SIAM J. Comput., 6(3):505–517, 1977. [20] A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, 42:230–265, 1936. [21] H. Wilf. Generatingfunctionology. A K Peters, Ltd., 3 edition, 2006. Available in https://www.math.upenn.edu/~wilf/DownldGF.html. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/79765 | - |
| dc.description.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。 我們針對九種類的輸入式子進行了相關的實驗。在實驗中，我們比較了我們實作的求解器與另外兩種求解器的效率。我們也測量了我們的求解器在各階段的執行時間，以此來分析我們的求解器的強項與缺點。實驗結果顯示我們的演算法與實作應該是正確的，且它們的效率整體而言優於其他的求解器。 | zh_TW |
| dc.description.provenance | Made available in DSpace on 2022-11-23T09:10:22Z (GMT). No. of bitstreams: 1 U0001-1708202102093200.pdf: 834182 bytes, checksum: a7210fccb4bef62ae6ffc00b40a020a1 (MD5) Previous issue date: 2021 | en |
| dc.description.tableofcontents | 口試委員會審定書 iii Acknowledgements v 摘要 vii Abstract ix 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Related works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2 Two variable logic 5 2.1 First order logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Two variable logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3 Conditional Independent Set 13 3.1 Definition and terminology . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.2 Algorithms for CIS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.1 Deterministic algorithm . . . . . . . . . . . . . . . . . . . . . . 14 3.2.2 Randomized algorithms . . . . . . . . . . . . . . . . . . . . . . 16 3.3 Reduction from SAT(FO2) to CIS . . . . . . . . . . . . . . . . . . . . . 17 3.3.1 Terminology . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3.2 Reduction to CIS . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4 Implementation 23 4.1 Scott normalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.2 Construction of the graph system . . . . . . . . . . . . . . . . . . . . . . 26 4.3 Deciding CIS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.3.1 Removing bad vertices . . . . . . . . . . . . . . . . . . . . . . . 28 4.3.2 Listing all the maximal independent sets . . . . . . . . . . . . . . 29 5 Experimental results 31 5.1 Setting and terminology . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 5.2 Experiments and results . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.2.1 Experiment 1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.2.2 Experiment 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 5.2.3 Experiment 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 5.2.4 Experiment 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 5.2.5 Experiment 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 5.2.6 Experiment 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 5.2.7 Experiment 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5.2.8 Experiment 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5.2.9 Experiment 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 5.3 Remarks on experimental results . . . . . . . . . . . . . . . . . . . . . . 42 6 Concluding remarks 45 Bibliography 47 A Definitions of the formulas in Chapter 5 49 | |
| dc.language.iso | en | |
| dc.subject | 條件性獨立集 | zh_TW |
| dc.subject | 可滿足性 | zh_TW |
| dc.subject | 雙變量邏輯 | zh_TW |
| dc.subject | satisfiability | en |
| dc.subject | conditional independent set | en |
| dc.subject | two variable logic | en |
| dc.title | 雙變量邏輯可滿足性的新解法與實作分析 | zh_TW |
| dc.title | A novel approach to the satisfiability of two-variable logic and its practical analysis | en |
| dc.date.schoolyear | 109-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 江介宏(Hsin-Tsai Liu),陳郁方(Chih-Yang Tseng) | |
| dc.subject.keyword | 雙變量邏輯,可滿足性,條件性獨立集, | zh_TW |
| dc.subject.keyword | two variable logic,satisfiability,conditional independent set, | en |
| dc.relation.page | 57 | |
| dc.identifier.doi | 10.6342/NTU202102417 | |
| dc.rights.note | 同意授權(全球公開) | |
| dc.date.accepted | 2021-08-18 | |
| dc.contributor.author-college | 電機資訊學院 | zh_TW |
| dc.contributor.author-dept | 資訊工程學研究所 | zh_TW |
| 顯示於系所單位： | 資訊工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| U0001-1708202102093200.pdf | 814.63 kB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。