The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


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/
Go to the corresponding LIPIcs Volume Portal

Wang, Hao-Ren ; Tu, Kuan-Hua ; Jiang, Jie-Hong Roland ; Scholl, Christoph

Quantifier Elimination in Stochastic Boolean Satisfiability

pdf-format:
LIPIcs-SAT-2022-23.pdf (0.8 MB)

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}
}

Keywords: Stochastic Boolean Satisfiability, Quantifier Elimination, Decision Procedure
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022
Supplementary Material: Software (Repository): https://github.com/NTU-ALComLab/elimssat archived at: https://archive.softwareheritage.org/swh:1:rev:076babed38a25f78805750192e9a54eba6ce9ef6

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI