Document Open Access Logo

Quantifier Elimination in Stochastic Boolean Satisfiability

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

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.23.pdf
  • Filesize: 0.77 MB
  • 17 pages

Document Identifiers

Author Details

Hao-Ren Wang
  • Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
Kuan-Hua Tu
  • Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
Jie-Hong Roland Jiang
  • Graduate Institute of Electronics Engineering / Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan
Christoph Scholl
  • Department of Computer Science, Universität Freiburg, Germany

Funding

This work was supported in part by the Ministry of Science and Technology of Taiwan under grants MOST 108-2221-E-002-144-MY3 and MOST 110-2224-E-002-011.

Cite AsGet BibTex

Hao-Ren Wang, Kuan-Hua Tu, Jie-Hong Roland Jiang, and Christoph Scholl. Quantifier Elimination in Stochastic Boolean Satisfiability. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.23

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Constraint and logic programming
Keywords
  • Stochastic Boolean Satisfiability
  • Quantifier Elimination
  • Decision Procedure

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Sundararaman Akshay, Supratik Chakraborty, Shubham Goel, Sumith Kulal, and Shetal Shah. What’s hard about Boolean functional synthesis? In Proceedings of the International Conference on Computer Aided Verification, pages 251-269, 2018. Google Scholar
  2. Kenneth Batcher. Sorting networks and their applications. In Proceedings of Spring Joint Computer Conference, pages 307-314, 1968. Google Scholar
  3. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable benchmarking: requirements and solutions. International Journal on Software Tools for Technology Transfer, pages 1-29, 2019. Google Scholar
  4. Robert Brayton and Alan Mishchenko. ABC: An academic industrial-strength verification tool. In Proceedings of the International Conference on Computer Aided Verification, pages 24-40, 2010. Google Scholar
  5. Marco Cadoli, Thomas Eiter, and Georg Gottlob. Default logic as a query language. IEEE Transactions on Knowledge and Data Engineering, pages 448-463, 1997. Google Scholar
  6. Pei-Wei Chen, Yu-Ching Huang, and Jie-Hong R. Jiang. A sharp leap from quantified boolean formula to stochastic Boolean satisfiability solving. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 3697-3706, 2021. Google Scholar
  7. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In International Conference on Theory and Applications of Satisfiability Testing, pages 502-503, 2003. Google Scholar
  8. Daniel Fremont, Markus Rabe, and Sanjit Seshia. Maximum model counting. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 3885-3892, 2017. Google Scholar
  9. Eric Freudenthal and Vijay Karamcheti. QTM: Trust management with quantified stochastic attributes. NYU Computer Science Technical Report TR2003-848, pages 1-14, 2003. Google Scholar
  10. Bishwamittra Ghosh, Debabrota Basu, and Kuldeep S. Meel. Justicia: A stochastic SAT approach to formally verify fairness. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 7554-7563, 2021. Google Scholar
  11. Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel. Manthan: A data driven approach for Boolean function synthesis. In Proceedings of the International Conference on Computer Aided Verification, pages 611-633, 2020. Google Scholar
  12. Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, and Kuldeep S. Meel. Engineering an efficient Boolean functional synthesis engine. In Proceedings of the International Conference on Computer-Aided Design, pages 1-9, 2021. Google Scholar
  13. Jinbo Huang. Combining knowledge compilation and search for conformant probabilistic planning. In Proceedings of the International Conference on Automated Planning and Scheduling, pages 253-262, 2006. Google Scholar
  14. Mikolás Janota and Joao Marques-Silva. Solving QBF by clause selection. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 325-331, 2015. Google Scholar
  15. Jie-Hong R. Jiang. Quantifier elimination via functional composition. In Proceedings of the International Conference on Computer Aided Verification, pages 383-397, 2009. Google Scholar
  16. Jie-Hong R. Jiang, Hsuan-Po Lin, and Wei-Lun Hung. Interpolating functions from large Boolean relations. In Proceedings of the International Conference on Computer-Aided Design, pages 779-784, 2009. Google Scholar
  17. Ajith K. John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi, and Sundararaman Akshay. Skolem functions for factored formulas. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, pages 73-80, 2015. Google Scholar
  18. Donald E. Knuth. The Art of Computer Programming. Fascicle 6: Satisfiability. Addison-Wesley, 2015. Google Scholar
  19. Andreas Kuehlmann, Malay K. Ganai, and Viresh Paruthi. Circuit-based Boolean reasoning. In Proceedings of the Design Automation Conference, pages 232-237, 2001. Google Scholar
  20. Nian-Ze Lee and Jie-Hong R. Jiang. Towards formal evaluation and verification of probabilistic design. In Proceedings of the International Conference on Computer-Aided Design, pages 340-347, 2014. Google Scholar
  21. Nian-Ze Lee and Jie-Hong R. Jiang. Dependency stochastic Boolean satisfiability: A logical formalism for NEXPTIME decision problems with uncertainty. Proceedings of the AAAI Conference on Artificial Intelligence, pages 3877-3885, 2021. Google Scholar
  22. Nian-Ze Lee, Yen-Shi Wang, and Jie-Hong R. Jiang. Solving stochastic Boolean satisfiability under random-exist quantification. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 688-694, 2017. Google Scholar
  23. Nian-Ze Lee, Yen-Shi Wang, and Jie-Hong R. Jiang. Solving exist-random quantified stochastic Boolean satisfiability via clause selection. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 1339-1345, 2018. Google Scholar
  24. Michael Littman, Judy Goldsmith, and Martin Mundhenk. The computational complexity of probabilistic planning. Journal of Artificial Intelligence Research, pages 1-36, 1998. Google Scholar
  25. Michael Littman, Stephen Majercik, and Toniann Pitassi. Stochastic Boolean satisfiability. Journal of Automated Reasoning, pages 251-296, 2001. Google Scholar
  26. Stephen M. Majercik and Byron Boots. DC-SSAT: A divide-and-conquer approach to solving stochastic satisfiability problems efficiently. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 416-422, 2005. Google Scholar
  27. Christos H. Papadimitriou. Games against nature. Journal of Computer and System Sciences, pages 288-301, 1985. Google Scholar
  28. Hagen Peters, Ole Schulz-Hildebrandt, and Norbert Luttenberger. Fast in-place, comparison-based sorting with CUDA: A study with bitonic sort. Concurrency and Computation: Practice and Experience, pages 681-693, 2011. Google Scholar
  29. Florian Pigorsch and Christoph Scholl. An AIG-based QBF-solver using SAT for preprocessing. In Proceedings of the Design Automation Conference, pages 170-175, 2010. Google Scholar
  30. Markus N. Rabe. Incremental determinization for quantifier elimination and functional synthesis. In Proceedings of the International Conference on Computer Aided Verification, pages 84-94, 2019. Google Scholar
  31. Ricardo Salmon and Pascal Poupart. On the relationship between satisfiability and Markov decision processes. In Proceedings of the Uncertainty in Artificial Intelligence Conference, pages 1105-1115, 2020. Google Scholar
  32. Friedrich Slivovsky. Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In Proceedings of the International Conference on Computer Aided Verification, pages 508-528, 2020. Google Scholar
  33. Fabio Somenzi. CUDD: CU decision diagram package release 2.4.2, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact