PSPACE 完備運動規劃之形式方法：以倉庫番為案例研究

Abstract

本研究將現實世界的倉庫番（Sokoban）遊戲轉化為模型檢測問題，並採用形式化方法進行求解。我們構建了一個端到端流程：解析關卡地圖、應用輕量級預處理、將謎題編碼為模型檢測實例，然後運行最先進的 PDR/IC3 求解器（ABC 和 rIC3）。通過比較兩種建模風格和兩種移動方向，並從搜尋求解器中引入基於規則的約束以加速求解，我們探討了實際應用中的關鍵問題。實驗結果顯示，該流程可解決 155 個 Microban 關卡中的 154 個，但由於狀態空間爆炸，只能處理 90 個更大型謎題集 XSokoban 中的 10 個。本研究報告了基於搜尋方法和形式化方法的主要發現，儘管對於非常大型的實例進行全面探索仍然困難，形式化方法在特定的問題中仍具備獨特的優勢。

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.