以隨機布林可滿足性編碼機率圖模型之問題

Encoding Probabilistic Graphical Model Problems into Stochastic Boolean Satisfiability

謝承翰(Cheng-Han Hsieh)

指導教授 ： 江介宏

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2022年)

https://doi.org/10.6342/NTU202200403

摘要

統計推論是具有許多應用的強力方法，雖然有許多推論工具能夠使用，解答複雜的量化結構推論問題依然十分困難。
隨機布林可滿足性(SSAT)是能編碼多項式空間複雜度中之隨機問題的形式，其近年來蓬勃發展並擁有越來越多應用。
我們利用隨機布林可滿足性問題來解決機率圖模型(PGMs)之推論，具體來說，我們開發了將機率圖模型之問題轉換成隨機布林可滿足性的系統性編碼方法。
此外，我們提出將任意機率值的隨機布林可滿足性標準化至只有0.5機率值的隨機布林可滿足性之方法.
實驗數據顯示，隨機布林可滿足性之解法能在複雜的推論問題中有效的與現有機率圖模型互補。

關鍵字

隨機布林可滿足性 ； 機率圖模型 ； 條件機率

並列摘要

Statistical inference is a powerful technique in various applications.
Although many statistical inference tools are available, answering inference queries involving complex quantification structures remains challenging.
Recently, solvers for Stochastic Boolean Satisfiability (SSAT), a powerful formalism allowing concise encodings of PSPACE decision problems under uncertainty, are under active development and applied in more and more applications.
In this work, we exploit SSAT solvers for the inference of Probabilistic Graphical Models (PGMs), an essential representation for probabilistic reasoning.
Specifically, we develop encoding methods to systematically convert PGM inference problems into SSAT formulas for effective solving.
% In addition, we generalize SSAT formula to represent conditional probability between variables.
In addition, a general SSAT formula with arbitrary probability can be normalized into a formula with only probability 0.5.
Experimental results demonstrate that, by using our encoding, SSAT-based solving can complement existing PGM tools in answering complex queries.

並列關鍵字

Stochastic Boolean satisfiability ； Probabilistic graphical models ； Conditional probability

參考文獻

[1] A. Bart, F. Koriche, J. Lagniez, and P. Marquis. An improved CNF encoding scheme for probabilistic inference. In European Conference on Artificial Intelligence, pages 613–621, 2016.

[2] M. Chavira and A. Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6):772–799, 2008.

[3] P. Chen, Y. Huang, and J. R. Jiang. A sharp leap from quantified boolean formula to stochastic boolean satisfiability solving. In AAAI Conference on Artificial Intelligence, pages 3697–3706, 2021.

[4] S. J. Chen, A. Choi, and A. Darwiche. An exact algorithm for computing the same-decision probability. In International Joint Conference on Artificial Intelligence, pages 2525–2531, 2013.

[5] A. Choi, Y. Xue, and A. Darwiche. Same-decision probability: A confidence measure for threshold-based decisions. International Journal of Approximate Reasoning, 53(9):1415–1428, 2012.