{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T22:25:05Z","timestamp":1748384705134},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,8]]},"abstract":"<jats:p>Stochastic Boolean Satisfiability (SSAT) is a powerful formalism to represent computational problems with uncertainly, such as belief network inference and propositional probabilistic planning. Solving SSAT formulas lies in the same complexity class (PSPACE-complete) as solving Quantified Boolean Formula (QBF). While many endeavors have been made to enhance QBF solving, SSAT has drawn relatively less attention in recent years. This paper focuses on random-exist quantified SSAT formulas, and proposes an algorithm combining binary decision diagram (BDD), logic synthesis, and modern SAT techniques to improve computational efficiency. Unlike prior exact SSAT algorithms, the proposed method can be easily modified to solve approximate SSAT by deriving upper and lower bounds of satisfying probability. Experimental results show that our method outperforms the state-of-the-art algorithm on random k-CNF formulas and has effective application to approximate SSAT on circuit benchmarks.<\/jats:p>","DOI":"10.24963\/ijcai.2017\/96","type":"proceedings-article","created":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T05:14:07Z","timestamp":1501218847000},"page":"688-694","source":"Crossref","is-referenced-by-count":4,"title":["Solving Stochastic Boolean Satisfiability under Random-Exist Quantification"],"prefix":"10.24963","author":[{"given":"Nian-Ze","family":"Lee","sequence":"first","affiliation":[{"name":"National Taiwan University, Taipei, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yen-Shi","family":"Wang","sequence":"additional","affiliation":[{"name":"National Taiwan University, Taipei, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[{"name":"National Taiwan University, Taipei, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"number":"26","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)","University of Technology Sydney (UTS)","Australian Computer Society (ACS)"],"acronym":"IJCAI-2017","name":"Twenty-Sixth International Joint Conference on Artificial Intelligence","start":{"date-parts":[[2017,8,19]]},"theme":"Artificial Intelligence","location":"Melbourne, Australia","end":{"date-parts":[[2017,8,26]]}},"container-title":["Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T07:52:14Z","timestamp":1501228334000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2017\/96"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2017,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2017\/96","relation":{},"subject":[],"published":{"date-parts":[[2017,8]]}}}