請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/87908完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 陳偉松 | zh_TW |
| dc.contributor.advisor | Tony Tan | en |
| dc.contributor.author | 陳法熏 | zh_TW |
| dc.contributor.author | Fa-Hsun Chen | en |
| dc.date.accessioned | 2023-07-31T16:15:00Z | - |
| dc.date.available | 2023-11-09 | - |
| dc.date.copyright | 2023-07-31 | - |
| dc.date.issued | 2023 | - |
| dc.date.submitted | 2023-06-23 | - |
| dc.identifier.citation | [1] V. Balabanov, H.-J. K. Chiang, and J.-H. R. Jiang. Henkin quantifiers and boolean formulae: A certification perspective of DQBF. TCS, 523:86–100, 2014.
[2] V. Balabanov and J.-H. R. Jiang. Reducing satisfiability and reachability to DQBF. In Talk given at International Workshop on Quantified Boolean Formulas, 2015. [3] R. Bloem, R. Könighofer, and M. Seidl. SAT-based synthesis methods for safety specs. VMCAI, pages 1–20, 2014. [4] K. Chatterjee, T. A. Henzinger, J. Otop, and A. Pavlogiannis. Distributed synthesis for LTL fragments. FMCAD, pages 18–25, 2013. [5] F.-H. Chen, S.-C. Huang, Y.-C. Lu, and T. Tan. Reducing NEXP-complete problems to DQBF. FMCAD, 2022. [6] D. R. Cok et al. The smt-libv2 language and tools: A tutorial. Language c, pages 2010–2011, 2011. [7] D.Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27, 1962. [8] U. Egly, M. Seidl, H. Tompits, S. Woltran, and M. Zolda. Comparing different prenexing strategies for quantified boolean formulas. SAT, pages 214–228, 2004. [9] B. Finkbeiner and L. Tentrup. Fast DQBF refutation. SAT, pages 243–251, 2014. [10] A. Fröhlich, G. Kovásznai, and A. Biere. A DPLL algorithm for solving DQBF. Proc. POS, 12, 2012. [11] A. Fröhlich, G. Kovásznai, A. Biere, and H. Veith. iDQ: Instantiation-based DQBF solving. POS-14. Fifth Pragmatics of SAT workshop, 27:103–116, 2014. [12] H. Galperin and A. Wigderson. Succinct representations of graphs. Inf. Control., 56(3):183—198, 1983. [13] A. Ge-Emst, C. Scholl, and R. Wimmer. Localizing quantifiers for DQBF. FMCAD, pages 184–192, 2019. [14] K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, and B. Becker. Equivalence checking of partial designs using dependency quantified boolean formulae. ICCD, pages 396–403, 2013. [15] K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, and B. Becker. Solving DQBF through quantifier elimination. In DATE, pages 1617–1622, 2015. [16] E. Grädel, P. G. Kolaitis, and M. Y. Vardi. On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic, 3(1):53–69, 1997. [17] B. Kiesl and M. Suda. A unifying principle for clause elimination in first-order logic. In CADE-26., pages 274–290, 2017. [18] L. Kovács and A. Voronkov. First-order interpolation and interpolating proof systems. In T. Eiter and D. Sands, editors, LPAR-21., volume 46 of EPiC Series in Computing, pages 49–64, 2017. [19] G. Kovásznai. What is the state-of-the-art in DQBF solving. In MaCS-16. Joint Conference on Mathematics and Computer Science, 2016. [20] A. Kuehlmann, V. Paruthi, F. Krohm, and M. Ganai. Robust boolean reasoning for equivalence checking and functional property verification. TCADICS, 21(12):1377–1394, 2002. [21] O. Kullmann and A. Shukla. Autarkies for DQCNF. In FMCAD, 2019. [22] C. Papadimitriou and M. Yannakakis. A note on succinct representations of graphs. Inf. Control., 71(3):181–185, 1986. [23] G. Peterson, J. Reif, and S. Azhar. Lower bounds for multiplayer noncooperative games of incomplete information. Computers and Mathematics with Applications, 41(7):957–992, 2001. [24] G. L. Peterson and J. H. Reif. Multiple-person alternation. SFCS-20., pages 348–363, 1979. [25] C. Scholl and B. Becker. Checking equivalence for partial implementations. DAC-38., pages 238–243, 2001. [26] C. Scholl, J.-H. Roland Jiang, R. Wimmer, and A. Ge-Ernst. A PSPACE subclass of dependency quantified boolean formulas and its effective solving. AAAI Conference on Artificial Intelligence, 33(01):1584–1591, 2019. [27] C. Scholl and R. Wimmer. Dependency quantified boolean formulas: An overview of solution methods and applications - extended abstract. In SAT, 2018. [28] J. Síč and J. Strejček. DQBDD: An efficient BDD-based DQBF solver. SAT, pages 535–544, 2021. [29] M. Soos. The CryptoMiniSat 5 set of solvers at SAT competition 2016. SAT Competition, page 28, 2016. [30] L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time (preliminary report). STOC, 1973. [31] J. Síč. Satisfiability of DQBF using binary decision diagrams. Master’s thesis, Masaryk University, Faculty of Informatics, Brno, 2020. SUPERVISOR : Jan Strejček. [32] L. Tentrup and M. N. Rabe. Clausal abstraction for DQBF. In SAT, pages 388–405, 2019. [33] G. S. Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967–1970, pages 466–483, 1983. [34] A. M. TURING. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230–265, 1937. [35] K. Wimmer, R. Wimmer, C. Scholl, and B. Becker. Skolem functions for DQBF. In ATVA, pages 395–411, 2016. [36] R. Wimmer, A. Karrenbauer, R. Becker, C. Scholl, and B. Becker. From DQBF to QBF by dependency elimination. In SAT, pages 326–343, 2017. [37] R. Wimmer, S. Reimer, P. Marin, and B. Becker. HQSpre–an effective preprocessor for QBF and DQBF. TACAS, 2017. [38] R. Wimmer, C. Scholl, and B. Becker. The (D) QBF preprocessor HQSpre–underlying theory and its implementation. JSAT, 11(1):3–52, 2019. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/87908 | - |
| dc.description.abstract | 精簡表示是指以對數大小的方式表示原本的問題，通常會導致問題的複雜度指數級增長。目前對精簡表示問題的已知解法是將它們先展開成標準表示，但這個過程可能會失去精簡表示隱含的附加信息。
對於解決精簡表示的非確定性多項式時間完備（NP-complete）問題，我們特別感興趣於兩種可滿足性問題是非確定性指數時間完備（NEXP-complete）的邏輯框架：雙變量邏輯（FO2）和相依量詞布林公式（DQBF）。雙變量邏輯為一階邏輯使用至多兩個變數的可判定（decidable）子集。相依量詞布林公式是廣義化的布林公式，可應用在軟硬體設計的驗證和合成中，近年來在求解方面已經取得了顯著進展。我們想要了解雙變量邏輯和相依量詞布林公式的求解器是否可用於幫助解決精簡表示的非確定性多項式時間完備問題。 本論文提出了從精簡表示的非確定性多項式時間完備問題到雙變量邏輯和相依量詞布林公式的規約（reduction）。我們還提出了用於求解相依量詞布林公式的演算法，該演算法在一些不可滿足的實例上比起已知的標準方法更具優勢。為了展示不同解法的效力，本文介紹了兩個具有精簡表示的圖列，並展示了它們在獨立集問題（independent set problem）和 漢米爾頓迴圈（Hamiltonian cycle problem）問題上的性質。我們還比較了我們的演算法與最先進的相依量詞布林公式求解器，DQBDD，在解決來自QBFEVAL 2020的競賽測資時的表現。 | zh_TW |
| dc.description.abstract | Succinct representation refers to a way of encoding information, which often leads to an exponential blow-up in complexity. The only known approach for solving succinctly represented problems is to decompress the problem into standard representation, which may discard some additional information implied by the succinct representation.
In this thesis, we focus on two logical frameworks whose satisfiability problems are NEXP-complete: two-variable logic (FO2) and dependency quantified boolean formula (DQBF). FO2 is a decidable fragment of first-order logic that uses at most two variables. DQBF is a generalization of boolean formulae that has applications in the verification and synthesis of hardware and software designs. There has been significant progress in solving DQBF in recent years. We aim to investigate whether solvers for FO$^2$ or DQBF can be used to solve instances derived from succinctly represented problems. This thesis proposes reductions from succinctly represented NP-complete problems to FO2 and DQBF instances and presents algorithms for solving DQBF. To demonstrate the effectiveness of various approaches for solving succinctly represented problems, this thesis presents two graph series with succinct representations and shows their properties on the independent set problem and the Hamiltonian cycle problem. Additionally, we compare our algorithm with the state-of-the-art DQBF solver, DQBDD, in the Competitive Evaluation of QBF Solvers (QBFEVAL 2020). | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2023-07-31T16:15:00Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2023-07-31T16:15:00Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 口試委員會審定書 iii
誌謝 v Acknowledgements vii 摘要 ix Abstract xi 1 Introduction 1 2 Preliminary 3 2.1 Succinct Representation 4 2.2 Two-Variable Logic 5 2.3 Quantified Boolean Formula 7 2.4 Dependency Quantified Boolean Formula 9 3 Reduction 13 3.1 Reductions from Succinctly Represented NP-complete Problems to FO2 14 3.2 Reductions from Succinctly Represented NP-complete Problems to DQBF 18 3.3 Insight from the Reductions 20 4 Algorithm for solving DQBF 23 4.1 First Algorithm: Naïve Reduction to SAT Instance 23 4.2 Second Algorithm: Forced Assignment Reduction to SAT Instance 25 4.3 Third Algorithm: Second Algorithm with Heuristics 26 5 Experiments with Succinctly Represented NP-complete Problems 29 5.1 Benchmarks 30 5.1.1 Differ Graph 30 5.1.2 Cover Graph 32 5.2 Solutions 33 5.3 Experiment Results 34 5.3.1 Succinctly Represented K-independent Set Problem 34 5.3.2 Succinctly Represented Hamiltonian Cycle Problem 38 6 Experiments with DQBF Solvers 41 6.1 Introduction to Benchmarks in DQBF solver track of QBFEVAL 2020 41 6.2 Experiment Results 42 7 Summary 45 Bibliography 47 | - |
| dc.language.iso | en | - |
| dc.subject | 雙變量邏輯 | zh_TW |
| dc.subject | 精簡表示 | zh_TW |
| dc.subject | 可滿足性 | zh_TW |
| dc.subject | 相依量詞布林公式 | zh_TW |
| dc.subject | succinct representation | en |
| dc.subject | FO2 | en |
| dc.subject | satisfiability | en |
| dc.subject | DQBF | en |
| dc.title | 精簡表示的NP完全問題與相依量詞布林公式 | zh_TW |
| dc.title | Succinctly Represented NP-complete Problems and DQBF | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 111-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 江介宏;王柏堯 | zh_TW |
| dc.contributor.oralexamcommittee | Jie-Hong Jiang;Bow-Yaw Wang | en |
| dc.subject.keyword | 精簡表示,可滿足性,雙變量邏輯,相依量詞布林公式, | zh_TW |
| dc.subject.keyword | succinct representation,satisfiability,FO2,DQBF, | en |
| dc.relation.page | 50 | - |
| dc.identifier.doi | 10.6342/NTU202301097 | - |
| dc.rights.note | 未授權 | - |
| dc.date.accepted | 2023-06-27 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 資訊網路與多媒體研究所 | - |
| 顯示於系所單位： | 資訊網路與多媒體研究所 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-111-2.pdf 未授權公開取用 | 605.93 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。