電路資訊於量詞布林函數求解中的重建與使用

Abstract

量詞布林可滿足性(QSAT)具有強大的編碼能力，計算理論中所有的PSPACE-Complete問題可自然且簡潔地編碼為量詞布林可滿足性問題。因此，量詞布林可滿足性問題持續吸引更多研究的關注，且近期也發展出許多高效的量詞布林(QBF)求解器，然而這些求解器仍不成熟，對於業界應用仍需要進一步的突破。 於量詞布林求解器中有兩個主要學習程序，包含有解學習(solution learning)與無解學習(conflict learning)。對於使用合取範式(conjunctive normal form)的量詞布林求解器，其中一主要的研究專注於縮小有解學習與無解學習之間對偶程度的差距(duality gap)，而此對偶程度的差距是源於無起始詞語資料(initial cube database)。 近期的研究顯示電路資訊可作為起始詞語資料以縮小對偶程度的差距，此技巧也被實作於兩個最前端的量詞布林求解器中，包含OOQ 與QELL 。OOQ 是第一個提出何謂可作為起始詞語資料的電路資訊，以及如何在使用歸結式(resolution-based)求解器中的有解學習使用電路資訊。另一方面，QELL 則提出了更普遍的可使用電路資訊的描述，且整合電路資訊於展開式(expansion-based)求解器的有解學習中。兩個求解器都展示電路資訊如何幫助加速求解效率。 然而，對於電路資訊的重建與使用仍有三個缺陷： 第一，可重建的電路資訊仍受限。 第二，僅電路資訊可被使用為起始詞語資料。 第三，電路資訊並無完整的使用於QELL 的有解學習中。 此論文對於此三個缺陷提出以下改進方法。 此論文提出如何重建出Tseitin轉換型式以外更多隱藏的電路資訊，以及提出用非電路資訊重建起始詞語資料，並提出對QELL 的有解學習中使用電路資訊的修改方法。新提出重建與使用電路資訊的方法實作於QELL 求解器中，且有提出例子證明此論文的貢獻。

Quantified Boolean Satisfiability (QSAT) is a powerful representation since any problem in PSPACE can be encoded naturally and compactly as QSAT. Due to its representational power, QSAT is gaining increasing research attention, and many effective quantified Boolean formula(QBF) solvers have been developed recently, yet these solvers remain premature and awaits further breakthroughs for industrial applications. There are two main procedures used for QBF solver, including solution learning and conflict learning. One of the main researches about conjunctive normal form based (CNF-based) solver focuses on how to bridge the duality gap between solution learning and conflict learning, while the duality gap results from the empty initial cube database. Recent research shows that circuit information can be used as initial cube database to bridge the gap, and such technique is implemented in two state-of-the-art QBF solvers, including OOQ and QELL. OOQ is the first QBF solver to propose the definition of usable circuit information for initial cube database, and how to utilize circuit information during solution learning in resolution-based solving style. On the other hand, QELL provides a more general characterization about usable circuit information and integrate circuit information with solution learning in an expansion-based solving style. Both solvers show how circuit information helps achieve exponential speed-up. However, the circuit information reconstruction and utilization are still incomplete in three aspects: First, the reconstructible circuit information is still restricted. Second, only circuit information can be used as initial cube database. Third, circuit information is not fully utilized in the solution learning of QELL. This thesis proposes improvement methods for these three aspects. This thesis shows how to recover more hidden circuit information in addition to Tseitin transformation pattern, and proposes a method to recover initial cubes uncovered by circuit information. This thesis also gives a modified solution learning method to utilize circuit information for QELL. The new proposed methods for reconstructing and utilizing circuit information are implemented in QELL solver, and instances are provided to evidence the contribution of this thesis.