- 學位論文
量詞布林公式: 演算法、應用、與隨機量詞延伸
Quantified Boolean Formula: Algorithms, Applications, and Extension to Randomized Quantification
摘要
量詞布林可滿足性 (Quantified Boolean satisfiability, QSAT) 是許多判定性問題很自然的表達，卻尚未有突破性解法可用於成熟的工業應用上。最近在量詞布林公式 (quantified Boolean formula, QBF) 的證明系統上的進展，銳化了我們對其複雜性的理解並顯露出一道改良求解器的光。某些基於公式展開法 (formula expansion) 的QBF求解器，在理論與實際上展現出相較非公式展開法求解器的更強大求解能力。然而，遞迴地展開苦惱於指數級的公式爆炸，仍需要小心處理。 我們提出了一個基於階層式帶有公式展開法風味的QBF求解器。使用了新的基於電路結構重建、完整或部分地全滿足性學習、核心展開、有限度遞迴的學習技術及其他方法去控制因公式展開帶來的公式爆炸。實驗顯示，我們的求解器原型與當代求解器有可比性，並在某些項目表現更佳。 在實際應用上，我們對兩種不同的問題，分別提出了基於 SAT 求解與 QBF 求解的新方法。 第一個問題是解碼器合成。編碼與解碼在資料處理上是很常見的行為。手動設計編碼器與解碼器難以避免錯誤及時間耗費。雖然已有良好的程序可從編碼器規範自動合成解碼器，但之前的方法只限定於無初始化的編碼器，其解碼器無法依賴於該編碼器的完整運行歷史。此解碼器存在條件無謂地過強，因為編碼器通常會被初始化於某些初始化狀態。我們展現了如何實際地合成有初始化狀態的解碼器。實驗結果顯示了優於先前方法能力且有效的解碼器合成法。 第二個問題是歸航序列 (Homing sequence) 導出。歸航序列導出在非確定性有限狀態機 (nondeterministic finite state machine, NFSM)的軟硬體系統測試與驗證中，有很重要的應用。不同於先前方法基於顯性樹搜尋，我們將歸航序列導出表示成QBF求解問題。此種表示方法利用緊湊的電路表達 NFSM 及歸航序列存在條件的QBF編碼，以達到有效的計算。隱性的電路表達有效地避免了顯性狀態列舉並且更加有可擴展性。我們探討了不同的編碼方式與QBF求解器在歸航序列導出的適用性。不同的計算方法與測試基準實驗，顯示了我們方法的一般性與可行性。 此外，我們延伸了 QBF 求解方法至隨機量詞，並且提出了一個新的演算法求解隨機布林可滿足性 (stochastic Boolean satisfiability, SSAT)問題。不同於之前基於 Davis-Putnam-Logemann-Loveland (DPLL) 搜尋的傳統SSAT演算法，我們的演算法將原方程式中的存在量詞消除，並改寫為只包含隨機量詞且滿足性機率相同的方程式。實驗的結果展現了此方法的可行性，但仍需要進一步的研究以解決在某些測試資料上的記憶體用量過大問題。
並列摘要
Quantified Boolean satisfiability (QSAT) is the natural formulation of many decision problems and yet awaits further breakthroughs to reach the maturity enabling industrial applications. Recent advancements in quantified Boolean formula (QBF) proof systems sharpen our understanding of their proof complexities and shed light on solver improvement. Particularly QBF solving based on formula expansion has been theoretically and practically demonstrated to be more powerful than non-expansion-based solving. However recursive expansion suffers from exponential formula explosion and has to be carefully managed. We propose a QBF solver using levelized SAT solving in the flavor of formula expansion. New learning techniques based on circuit structure reconstruction, complete and incomplete ALLSAT learning, core expansion, bounded recursion, and other methods are devised to control formula growth. Experimental results on application benchmarks show that our prototype implementation is comparable with state-of-the-art solvers and outperforms other solvers in certain instances. For application use, we proposed two new methods for two different problems by SAT and QBF solving respectively. The first problem is decoder synthesis. Encoding and decoding are common practices in the data processing. Designing encoder and decoder circuitry manually can be error-prone and time-consuming. Although great progress has been made on automating decoder synthesis from its encoder specification, the prior specification was limited to an uninitialized encoder only, whose decoder cannot depend on the entire execution history of the encoder. Prior decoder existence condition is unnecessarily stringent as encoders are often initialized with respect to some initial states. We show how decoders of initialized encoders can be practically synthesized. Experimental results demonstrate effective decoder synthesis of initialized encoders, beyond existing methods' capabilities. The second problem is homing sequence derivation. Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in software/hardware system testing and verification. Unlike prior methods based on explicit tree-based search, in this work, we formulate the derivation of a preset/adaptive homing sequence in terms of quantified Boolean formula (QBF) solving. This formulation exploits compact circuit representation of NFSMs and QBF encoding of the existing condition of homing sequence for effective computation. The implicit circuit representation effectively avoids explicit state enumeration and can be more scalable. Different encoding schemes and QBF solvers are evaluated for their suitability in homing sequence derivation. Experiments on various computation methods and benchmarks show the generality and feasibility of the proposed approach. In addition, we extended the QBF solving algorithm with randomized quantification and proposed a new algorithm to solve the stochastic Boolean satisfiability (SSAT) problem. In contrast to the conventional SSAT-solving approaches based on Davis-Putnam-Logemann-Loveland (DPLL) algorithm, our approach is a rewrite-based algorithm that eliminates all existential quantifiers and creates an SSAT formula having the same satisfying probability. Experiments show the solving capability of the proposed approach, however, further research is needed to solve the memory explosion issue on some benchmarks.