請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/98764完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 黃鐘揚 | zh_TW |
| dc.contributor.advisor | Chung-Yang Huang | en |
| dc.contributor.author | 劉虹伶 | zh_TW |
| dc.contributor.author | Hung-Ling Liu | en |
| dc.date.accessioned | 2025-08-19T16:06:48Z | - |
| dc.date.available | 2025-08-20 | - |
| dc.date.copyright | 2025-08-19 | - |
| dc.date.issued | 2025 | - |
| dc.date.submitted | 2025-08-06 | - |
| dc.identifier.citation | [1] A. Biere. Bounded model checking. In Handbook of satisfiability, pages 739–764. IOS press, 2021.
[2] A. Biere, K. Heljanko, and S. Wieringa. AIGER 1.9 and beyond. Technical Report 11/2, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria, 2011. [3] A. Biere, M. Preiner, et al. btor2tools: A tool suite for the BTOR2 format. https://github.com/hwmcc/btor2tools, 2025. Accessed: 2025-07-14. [4] M. Bofill, C. Borralleras, J. Espasa, and M. Villaret. On grid graph reachability and puzzle games. arXiv preprint arXiv:2310.01378, 2023. [5] R. K. Brayton and A. Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, 2010. [6] J. Culberson. Sokoban is pspace-complete. 1997. [7] N. Een, A. Mishchenko, and R. Brayton. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-Aided Design (FMCAD), pages 125–134, 2011. [8] Hardware Model Checking Competition. HWMCC 2024. https://hwmcc.github.io/, 2024. Accessed: 2025-07-18. [9] A. Junghanns and J. Schaeffer. Sokoban: Enhancing general single-agent search methods using domain knowledge. Artificial Intelligence, 129(1):219–251, 2001. [10] A. Myers. XSokoban. http://www.cs.cornell.edu/andru/xsokoban.html. Accessed: 2025‑07‑17. [11] A. Niemetz, M. Preiner, C. Wolf, and A. Biere. Btor2, btormc and boolector 3.0. In International Conference on Computer Aided Verification, pages 587–595. Springer, 2018. [12] S. Quer. Back to basics: Solving games with sat. Advances in Electrical and Computer Engineering, 16(3):91–99, 2016. [13] Y. Shoham and J. Schaeffer. The fess algorithm: A feature based approach to single-agent search. In 2020 IEEE Conference on Games (CoG), pages 96–103, 2020. [14] Y. Su, Q. Yang, Y. Ci, T. Bu, and Z. Huang. The ric3 hardware model checker. In R. Piskac and Z. Rakamarić, editors, Computer Aided Verification, pages 185–199, Cham, 2025. Springer Nature Switzerland. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/98764 | - |
| dc.description.abstract | 本研究將現實世界的倉庫番（Sokoban）遊戲轉化為模型檢測問題，並採用形式化方法進行求解。我們構建了一個端到端流程：解析關卡地圖、應用輕量級預處理、將謎題編碼為模型檢測實例，然後運行最先進的 PDR/IC3 求解器（ABC 和 rIC3）。通過比較兩種建模風格和兩種移動方向，並從搜尋求解器中引入基於規則的約束以加速求解，我們探討了實際應用中的關鍵問題。實驗結果顯示，該流程可解決 155 個 Microban 關卡中的 154 個，但由於狀態空間爆炸，只能處理 90 個更大型謎題集 XSokoban 中的 10 個。本研究報告了基於搜尋方法和形式化方法的主要發現，儘管對於非常大型的實例進行全面探索仍然困難，形式化方法在特定的問題中仍具備獨特的優勢。 | zh_TW |
| dc.description.abstract | This work turns the real-world Sokoban puzzle into a model-checking problem and tackles it with formal methods. We build an end-to-end flow: parse the map, apply lightweight preprocessing, encode the puzzle as a model‑checking instance, and run state-of-the-art PDR/IC3 solvers (ABC and rIC3). Practical issues are examined by comparing two modeling styles and two move directions, and by importing rule-based constraints from search solvers to speed up. Experiments show that the flow solves 154 of 155 Microban cases, yet handles only 10 of 90 larger puzzle set XSokoban because of the state-space explosion. The study reports findings for both search-based and formal approaches. Although exhaustive exploration remains difficult on very large instances, the formal method provides unique advantages in certain types of problems. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2025-08-19T16:06:48Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2025-08-19T16:06:48Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 摘要 i
Abstract ii Contents iii List of Figures vi List of Tables viii Chapter 1 Introduction 1 1.1 Background and Motivations . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Contributions of this Thesis . . . . . . . . . . . . . . . . . . . . . . 2 Chapter 2 Problem Description and Related Work 3 2.1 The Sokoban Game . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Problem Description . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3.1 Search-Based Methods . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3.2 Formal Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Chapter 3 Preliminaries 8 3.1 Model Checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Bounded Model Checking (BMC) . . . . . . . . . . . . . . . . . . . 9 3.3 Property Directed Reachability (PDR/IC3) . . . . . . . . . . . . . . 10 3.4 Verification Tools and Modeling Format . . . . . . . . . . . . . . . . 12 Chapter 4 Solving Sokoban with Formal Methods 14 4.1 Overview of the Flow . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2 Preprocessing Phase . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2.1 Deadlocks in Forward and Backward Search . . . . . . . . . . . . . 16 4.2.2 Treating Settled and Fixed Boxes as Walls . . . . . . . . . . . . . . 17 4.3 Modeling Phase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.3.1 Inputs and State Variables . . . . . . . . . . . . . . . . . . . . . . . 18 4.3.2 Predicate for the Initial Position . . . . . . . . . . . . . . . . . . . 18 4.3.3 Transition Relation for the Legal Moves . . . . . . . . . . . . . . . 18 4.3.4 Safety Property for the Game Target . . . . . . . . . . . . . . . . . 20 4.4 Add-on Rules Phase . . . . . . . . . . . . . . . . . . . . . . . . . . 20 4.5 Solving Phase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Chapter 5 Implementation Issues 22 5.1 Modeling Variants . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 5.1.1 Action-Input Encoding . . . . . . . . . . . . . . . . . . . . . . . . 23 5.1.2 Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.2 Move Direction: Forward vs. Backward Approaches . . . . . . . . . 26 5.2.1 Pull-Backward Modeling . . . . . . . . . . . . . . . . . . . . . . . 26 5.2.2 Case Study . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Chapter 6 Enhancing PDR with Rule-Based Constraints 29 6.1 Deadlock Table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 6.2 Retrograde Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 31 6.3 Multi-Steps in Single Timeframe . . . . . . . . . . . . . . . . . . . . 33 6.4 Discussion on PDR . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 6.4.1 Empirical Findings on Rule-Based Constraints . . . . . . . . . . . . 36 6.4.2 Limits on Rule Encoding . . . . . . . . . . . . . . . . . . . . . . . 37 Chapter 7 Case Study of PDR 40 7.1 Easy Case: When PDR Works Exceptionally Well . . . . . . . . . . 40 7.2 Hard Cases: Where PDR Struggles . . . . . . . . . . . . . . . . . . 43 Chapter 8 Experimental Results 46 8.1 Benchmark Descriptions (Microban, XSokoban) . . . . . . . . . . . 47 8.2 Experimental Results on Microban . . . . . . . . . . . . . . . . . . . 48 8.2.1 Comparison among Formal Methods . . . . . . . . . . . . . . . . . 48 8.2.2 Comparison between Formal and Search-Based Solvers . . . . . . . 50 8.3 Experimental Results on Xsokoban . . . . . . . . . . . . . . . . . . 52 8.4 Effect of AIG Optimization . . . . . . . . . . . . . . . . . . . . . . 53 8.5 Detecting Unsolvable Cases with Formal Methods . . . . . . . . . . 54 Chapter 9 Conclusion 57 9.1 Formal Methods vs. Search-Based Solvers . . . . . . . . . . . . . . 57 9.2 Reflections on Sokoban as a Case Study . . . . . . . . . . . . . . . . 58 9.3 Positioning Formal Methods in Practice . . . . . . . . . . . . . . . . 58 References 60 | - |
| dc.language.iso | en | - |
| dc.subject | 形式化方法 | zh_TW |
| dc.subject | 倉庫番 | zh_TW |
| dc.subject | 性質導向可達性技術 | zh_TW |
| dc.subject | 模型檢查 | zh_TW |
| dc.subject | 邏輯電路 | zh_TW |
| dc.subject | PDR | en |
| dc.subject | Formal Method | en |
| dc.subject | Logic Circuits | en |
| dc.subject | Model Checking | en |
| dc.subject | Sokoban | en |
| dc.title | PSPACE 完備運動規劃之形式方法：以倉庫番為案例研究 | zh_TW |
| dc.title | Formal Methods for PSPACE-Complete Motion Planning: A Sokoban Case Study | en |
| dc.type | Thesis | - |
| dc.date.schoolyear | 113-2 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 江介宏;李念澤;王柏堯 | zh_TW |
| dc.contributor.oralexamcommittee | Jie-Hon Jiang;Nian-Ze Lee;Bow-Yaw Wang | en |
| dc.subject.keyword | 形式化方法,倉庫番,性質導向可達性技術,模型檢查,邏輯電路, | zh_TW |
| dc.subject.keyword | Formal Method,Sokoban,PDR,Model Checking,Logic Circuits, | en |
| dc.relation.page | 61 | - |
| dc.identifier.doi | 10.6342/NTU202503823 | - |
| dc.rights.note | 同意授權(限校園內公開) | - |
| dc.date.accepted | 2025-08-12 | - |
| dc.contributor.author-college | 電機資訊學院 | - |
| dc.contributor.author-dept | 電機工程學系 | - |
| dc.date.embargo-lift | 2025-08-20 | - |
| 顯示於系所單位： | 電機工程學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| ntu-113-2.pdf 授權僅限NTU校內IP使用（校園外請利用VPN校外連線服務） | 12.41 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。