- 學位論文
論隨機布林可滿足性：決策程序、廣義化、與應用
Stochastic Boolean Satisfiability: Decision Procedures, Generalization, and Applications
摘要
隨機布林可滿足性（SSAT）是一種豐富的邏輯語言，可用於表達具有機率性的計算問題，例如貝氏網絡推論，命題式機率性規劃，和部分可觀察馬可夫決策過程（POMDP）。求解SSAT公式之複雜度屬於多項式空間完全性複雜度類別（PSPACE-complete complexity class），與求解量化布林公式（QBF）相同。儘管具有廣泛的應用和深刻的理論價值，SSAT在文獻中所引起的關注較SAT或QBF稀少。 我們在機率性設計的正規驗證問題中找到SSAT的新應用。機率性設計以及近似性設計是一種新興的計算準則，可用來容忍VLSI系統在奈米製程下的元件變異性。儘管相關文獻對近似性設計進行了許多探討， 機率性設計則很少受到關注。我們為機率性設計提出了機率性質評估框架並利用隨機存在和存在隨機的量化SSAT公式求解，分別進行平均情況和最壞情況分析。據我們所知，這是文獻中首次將SSAT應用於VLSI系統分析。 受以上VLSI系統應用的推動，我們提出了新的演算法來求解隨機存在和存在隨機的量化SSAT公式。不同於基於Davis-Putnam-Logemann-Loveland（DPLL）搜尋的傳統SSAT演算法，我們利用當代SAT或QBF求解技術和模型計數以提高計算效率。與之前基於DPLL搜尋的準確SSAT演算法不同，我們的演算法能夠近似地求解SSAT公式，計算其滿足機率的上下限。 我們在開源SSAT求解器reSSAT和erSSAT中實作所提出的新演算法。 實驗結果顯示reSSAT和erSSAT求解器的性能優於文獻中的SSAT求解器。在文獻中的求解器無法計算出準確答案的情況下，它們也能提供有用的上下限。 儘管在不同領域都有許多應用，SSAT仍受限於其PSPACE complexity class的描述能力。更複雜的問題，例如非確定指數時間完全性（NEXPTIME-complete）的分散式POMDP（decentralized POMDP, Dec-POMDP），則無法用SSAT簡潔地表示。為了提供此類問題一個邏輯框架，我們借鏡了同為NEXPTIME-complete的依賴性QBF（dependency QBF, DQBF）。我們推廣SSAT並命名該推廣框架為依賴性SSAT（dependency SSAT, DSSAT），同時證明DSSAT也是NEXPTIME-complete。我們展示了DSSAT在機率或近似性設計的合成中的潛在應用，以及針對Dec-POMDP問題的編碼。我們希望通過建立理論基礎來鼓勵DSSAT求解器的開發。
並列摘要
Stochastic Boolean satisfiability (SSAT) is an expressive language to formulate computational problems with randomness, such as the inference of Bayesian networks, propositional probabilistic planning, and partially observable Markov decision process (POMDP). Solving an SSAT formula lies in the PSPACE-complete complexity class, the same as solving a quantified Boolean formula (QBF). Despite its broad applications and profound theoretical values, SSAT has drawn relatively less attention compared to SAT or QBF. We identify new applications of SSAT in the formal verification of probabilistic design. Probabilistic design, as well as approximate design, is an emerging computational paradigm to accept the device variability of VLSI systems in the nanometer regime, which imposes serious challenges to the design and manufacturing of reliable systems. Despite recent intensive study on approximate design, probabilistic design receives relatively few attentions. We formulate the framework of probabilistic property evaluation for probabilistic design and exploit random-exist and exist-random quantified SSAT solving to approach the average-case and worst-case analyses, respectively. To the best of our knowledge, this is the first attempt that applies SSAT to analyze VLSI systems. Motivated by the above emerging applications, we propose novel algorithms to solve random-exist and exist-random quantified SSAT formulas. These two fragments of SSAT have important AI applications in the reasoning of Bayesian networks and the search of an optimal strategy for probabilistic conformant planning. In contrast to the conventional SSAT-solving approaches based on Davis-Putnam-Logemann-Loveland (DPLL) search, we take advantage of modern techniques for SAT/QBF solving and model counting to improve the computational efficiency. Moreover, unlike the prior DPLL-based exact algorithms for SSAT solving, the proposed algorithms are able to solve an SSAT formula approximately by deriving upper or lower bounds of its satisfying probability. The proposed algorithms are implemented in the open-source SSAT solvers reSSAT and erSSAT. Our evaluation shows that reSSAT and erSSAT solvers outperform the state-of-the-art SSAT solver on various formulas in both run-time and memory usage. They also provide useful bounds for cases where the state-of-the-art solver fails to compute exact answers. In spite of its various applications, SSAT is limited by its descriptive power within the PSPACE complexity class. More complex problems, such as the NEXPTIME-complete decentralized POMDP (Dec-POMDP), cannot be succinctly encoded with SSAT. To provide a logical formalism for such problems, we extend the dependency quantified Boolean formula (DQBF), a representative problem in the NEXPTIME-complete class, to its stochastic variant, named dependency SSAT (DSSAT), and show that DSSAT is also NEXPTIME-complete. We demonstrate potential applications of DSSAT in the synthesis of probabilistic/approximate design and the encoding of Dec-POMDP problems. We hope to encourage solver development with the established theoretical foundations.
參考文獻
延伸閱讀
- Hsieh, C. H. (2022). 以隨機布林可滿足性編碼機率圖模型之問題 [master's thesis, National Taiwan University]. Airiti Library. https://doi.org/10.6342/NTU202200403
- 郭郁寬（2019）。利用隨機規劃模式求解考量旅客選擇之動態機位控管問題〔碩士論文，國立交通大學〕。華藝線上圖書館。https://www.airitilibrary.com/Article/Detail?DocID=U0030-0306202016370221
- Tu, K. H. (2022). 量詞布林公式: 演算法、應用、與隨機量詞延伸 [doctoral dissertation, National Taiwan University]. Airiti Library. https://doi.org/10.6342/NTU202200071
- Hsu, Y. R. (2021). 使用自適應量子啟發式禁忌搜尋演算法解決具權重之投資組合最佳化問題並使用趨勢值及考量投資者心情波動之新穎指標 [master's thesis, National Chi Nan University]. Airiti Library. https://doi.org/10.6837/ncnu202100360
- 孫積賢（2012）。Application of Stochastic Optimization Methods to the Inverse Scattering of 2-D scatterers〔博士論文，淡江大學〕。華藝線上圖書館。https://doi.org/10.6846/TKU.2012.00695