透過您的圖書館登入
IP:44.200.237.112
  • 學位論文

量詞布林公式之歸結證明系統與正反模型萃取

Certification in Quantified Decision Procedures

指導教授 : 江介宏

摘要


可滿足性(Satisfiability, SAT)測試在當代的自動化推理領域扮演著關鍵的角色。在近十年眾多研究人員的努力下,SAT求解技術已臻成熟而能有效擴展解決大型問題,成功地被廣泛運用於各式業界的邏輯求解問題上。相較於SAT,量化布林公式(Quantified Boolean Formula, QBF)允許存在性量詞與所有性量詞對變量的量化設限,因而擴展了命題邏輯公式的表達力,能更簡潔地表示約束式。除了在正規驗證的應用,QBF在電子設計自動化、人工智慧規劃問題、對弈賽局等計算機科學領域皆有廣泛的應用。 許多SAT的有效求解方法已被提出,包括具各種學習技術的搜尋方法(例如,衝突驅動的條件學習),語法重寫方法(例如,歸結規則),不同的預處理技術(例如,純文本消除),等等。許多這些技術被修改採用於QBF求解(例如,基於學習搜尋的演算法, Q-歸結規則等擴展)。儘管其與SAT求解有相似處, QBF求解因其所具的量化功能有獨特的特殊性,QBF求解在計算複雜度上屬PSPACE-complete,為多項式階層中最困難的問題,被視為比SAT求解等的NP-complete類別更困難許多。 QBFs的認證近來引起極大的關注:它(QBF語法認證)不僅於用來驗證QBF求解的正確性,(QBF語意認證)更能夠直接地提供許多合成應用上所需的資訊。QBF的語意認證可以是,例如,在兩人對弈賽局中的穩贏策略,在關係確定化問題中的函數式答案,和其它實際對應。縱使QBF的求解和認證有極高的重要性,其相關的演算法仍不成熟,許多關鍵問題仍然沒有很好的解法。 在本論文,我們總覽各式QBF求解和認證技術,提出新的QBF證明系統和認證方法,並以實驗證實新方法相較於現有方法的優越性。我們的主要貢獻包括開發 ,基於Q-歸結規則,新的QBF證明系統與其語法認證、開發高效的演算法自擴展的語法認證提取語意認證、開發優化演算法化簡語意認證、開發Dependency QBF(DQBF)語意分類方法等成果。除理論貢獻外,我們還以實驗表明所提出方法在當前應用上的具體實用價值。

並列摘要


Satisfiability (SAT) plays one of the key roles in the modern automated reasoning. For the past decade a huge success in SAT solving was achieved by researchers, and nowadays SAT-based decision algorithms scale well for many real-world applications. Quantified Boolean Formulas (QBFs) extend formulas of propositional logic by allowing existential and universal quantifications over variables. Quantifiers make QBF more expressive and allow a more compact constraints representation compared to SAT. In addition to problems encountered in formal verification, QBF has applications in planning, two-player games, electronic design automation, and other fields of computer science. Many methods have been proposed for efficient SAT solving, including search-based solving with different learning techniques (e.g., conflict driven clause learning), syntactic rewriting methods (e.g., resolution rules), various preprocessing techniques (e.g., variable elimination), and so on. Many of these techniques were then adapted for QBF evaluation (e.g., extensions of search-based algorithms, introduction of Q-resolution, etc). Despite its similarities to SAT solving, evaluating QBFs has its unique features related to the quantification nature. Certification of QBFs is of a great interest: Not only it confirms the answer provided by the solver (e.g., by providing syntactic Q-resolution proof), but more importantly directly provides information required in many synthesis applications (e.g., by returning a semantic model). Semantic QBF certificates can serve as a winning strategy in two-player games, the functional representation of a relation in a determinization problem, and other applications. Despite the importance of QBF evaluation and certification, solving algorithms remain immature, and many related issues are not well studied yet. In this work we provide an overview of different QBF solving and certifying techniques, and propose novel approaches that experimentally show improvements over existing ones. Our main contributions include developing new QBF proof systems and building corresponding syntactic certificates based on Q-resolution, providing efficient algorithms for semantic certificates extraction from various syntactic proofs, introducing new optimization heuristics for semantic certificates minimization, and a semantic classification method for dependency QBFs (DQBFs). Along with theoretical achievements, conducted experiments show that proposed methods can be useful in modern applications, therefore forming solid practical values.

參考文獻


[32] Alan Mishchenko, Satrajit Chatterjee, and Robert K. Brayton. Dag-aware AIG rewriting a fresh look at combinational logic synthesis. In Proceedings of the 43rd Design Automation Conference, DAC 2006, San Francisco, CA, USA, July 24-28, 2006, pages 532–535, 2006.
[12] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Hand- book of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
[1] Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009.
[2] Valeriy Balabanov, Hui-Ju Katherine Chiang, and Jie-Hong R. Jiang. Henkin quantifiers and boolean formulae: A certification perspective of DQBF. Theor. Comput. Sci., 523:86–100, 2014.
[5] Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF Certification and Its Applications. Formal Methods in System Design, 41:45–65, 2012.

延伸閱讀