量詞布林公式求解之認證統合

量化布林公式（QBF）評估是理論和實用計算機科學領域的核心問題之一。理論上，QBF求解有極高的複雜度，更精確來說是計算理論中所的PSPACE-Complete的問題。在實務上，各種應用問題(如邏輯合成，硬體模型檢查，軟體合成，機器人規劃，賽局問題等)能被精簡地編碼成QBF再進而求解。雖然最近許多行之有效的QBF求解器已被開發，其中只有少數能為他們的答案提供正確性的認證。 QBF認證的重要性有兩方面：首先，它保證了QBF求解器計算上的正確性。其次，也許是更重要的因素，適當形式的認證（特別是Skolem與Herbrand函數）能使某些合成的任務得以被完成，例如，在邏輯合成應用中從布林關係萃取函數，在賽局理論中求取穩贏的策略等。已知的QBF認證有各種形式：對為真的QBF（true QBF）認證可以是詞語式的歸結證明（cube resolution proof）或Skolem函數；對為偽的QBF（false QBF）認證可以是子句式的歸結證明（clause resolution proof）。現今對QBF認證的了解有兩點極大的缺陷：第一，false QBF無相對應於Skolem函數的認證。第二，歸結證明認證與Skolem函數認證互為獨立無法連結。本論文解決了這兩個未知問題：一來找出false QBF相對應於Skolem函數的Herbrand函數認證，二來建立起由歸結證明認證轉換至Skolem/Herbrand函數認證的有效演算法。實驗顯示我們的方法結合現有的QBF求解器可以產生更多的Skolem模型和Herbrand反模型，是以往所無法求得的。我們期望本論文所獲致的結果將可能會進一步帶動QBF的研究及於現代合成和驗證方法上的應用。

關鍵字

量化布林公式； QBF ；認證；分解； Skolem函數； Herbrand函數

並列摘要

Quantified Boolean Formulas (QBFs) have been widely used in many practical applications, such as: model checking, automated planning, non-monotonic reasoning, scheduling, multi-agent scenarios, etc. Many effective state-of-the-art QBF tools have been developed. However only a few of the modern solvers can certify their answer. The importance of QBF certification is two-fold. First, it ensures the correctness of a solver. Second, perhaps more importantly, if the certificate is in an appropriate form (specifically, in Skolem/Herbrand functions), it enables certain synthesis tasks. The accepted types of certificates are cube resolution proofs and Skolem functions for true QBFs, and clause resolution proofs for false QBFs. The current understanding about QBF certification is incomplete in two aspects. First, the certificate of false QBFs has the missing Skolem-function counterpart. Second, the connection between resolution proofs and Skolem functions remains unclear. These two open questions are resolved in this thesis by bridging the connection between the syntactic (resolution) certificates and the semantic (Skolem-function) certificates, and by piecing out the missing Herbrand-function certificates for false QBFs. Essentially we derive Skolem models from cube resolution proofs and Herbrand countermodels from clause resolution proofs for true and false QBFs, respectively. Practical experience suggests that our approach in combination with some existing QBF solvers can generate many more Skolem models and Herbrand countermodels than prior methods. It enables applications, such as: relation determinization problems, maximum sequential diameter problems, and other. We hope, that this work will encourage QBF-based solving methods in modern logic-synthesis and verification problems.

並列關鍵字

Quantified Boolean Formula ； QBF evaluation ； certificate ； q-resolution ； Skolem function ； Herbrand function

參考文獻

[1] Marco Benedetti. sKizzo: a Suite to Evaluate and Certify QBFs. In Proc. of

the 20th International Conference on Automated Deduction, 2005.

Automatic hardware synthesis from specifications: A case study. In Proc. De-

sign Automation and Test in Europe, 2007.

[5] Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential

國際替代計量

量詞布林公式求解之認證統合

全文下載

主題瀏覽