License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.23
URN: urn:nbn:de:0030-drops-166970
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16697/
Wang, Hao-Ren ;
Tu, Kuan-Hua ;
Jiang, Jie-Hong Roland ;
Scholl, Christoph
Quantifier Elimination in Stochastic Boolean Satisfiability
Abstract
Stochastic Boolean Satisfiability (SSAT) generalizes quantified Boolean formulas (QBFs) by allowing quantification over random variables. Its generality makes SSAT powerful to model decision or optimization problems under uncertainty. On the other hand, the generalization complicates the computation in its counting nature. In this work, we address the following two questions: 1) Is there an analogy of quantifier elimination in SSAT, similar to QBF? 2) If quantifier elimination is possible for SSAT, can it be effective for SSAT solving? We answer them affirmatively, and develop an SSAT decision procedure based on quantifier elimination. Experimental results demonstrate the unique benefits of the new method compared to the state-of-the-art solvers.
BibTeX - Entry
@InProceedings{wang_et_al:LIPIcs.SAT.2022.23,
author = {Wang, Hao-Ren and Tu, Kuan-Hua and Jiang, Jie-Hong Roland and Scholl, Christoph},
title = {{Quantifier Elimination in Stochastic Boolean Satisfiability}},
booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
pages = {23:1--23:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-242-6},
ISSN = {1868-8969},
year = {2022},
volume = {236},
editor = {Meel, Kuldeep S. and Strichman, Ofer},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16697},
URN = {urn:nbn:de:0030-drops-166970},
doi = {10.4230/LIPIcs.SAT.2022.23},
annote = {Keywords: Stochastic Boolean Satisfiability, Quantifier Elimination, Decision Procedure}
}
