https://scholars.lib.ntu.edu.tw/handle/123456789/632105
標題: | A Sharp Leap from Quantified Boolean Formula to Stochastic Boolean Satisfiability Solving | 作者: | Chen P.-W Huang Y.-C JIE-HONG JIANG |
公開日期: | 2021 | 卷: | 5A | 起(迄)頁: | 3697-3706 | 來源出版物: | 35th AAAI Conference on Artificial Intelligence, AAAI 2021 | 摘要: | Stochastic Boolean Satisfiability (SSAT) is a powerful representation for the concise encoding of quantified decision problems with uncertainty. While it shares commonalities with quantified Boolean formula (QBF) satisfiability and has the same PSPACE-complete complexity, SSAT solving tends to be more challenging as it involves expensive model counting, a.k.a. Sharp-SAT. To date, SSAT solvers, especially those imposing no restrictions on quantification levels, remain much lacking. In this paper, we present a new SSAT solver based on the framework of clause selection and cube distribution previously proposed for QBF solving. With model counting integrated and learning techniques strengthened, our solver is general and effective. Experimental results demonstrate the overall superiority of the proposed algorithm in both solving performance and memory usage compared to the state-of-the-art solvers on a number of benchmark formulas. Copyright © 2021, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85103013082&partnerID=40&md5=70a222f67c0a81369e6c9c5a07e0192a https://scholars.lib.ntu.edu.tw/handle/123456789/632105 |
SDG/關鍵字: | Artificial intelligence; Benchmarking; Learning systems; Stochastic systems; Boolean formula satisfiability; Decision problems; Expensive models; Model Counting; PSPACE-complete; Quantified Boolean formulas; Satisfiability solvers; Satisfiability solving; Stochastic boolean satisfiability; Uncertainty; Boolean functions |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。