Document Open Access Logo

Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition

Authors Jung-Cheng Lin , Chia-Hsuan Su , Jie-Hong R. Jiang , Hiroshi Unno

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.24.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Stochastic Satisfiability Modulo Theories (SSMT)
  • Cylindrical Algebraic Decomposition (CAD)
  • Quantifier Elimination

Metrics

Abstract

Stochastic Satisfiability Modulo Theories (SSMT) has traditionally focused on the interplay between existential and randomized quantifiers, typically relying on numerical sampling or approximations. We present a generalized SSMT framework that integrates universal quantification, lifting the formalism to a robust stochastic game-theoretic setting. By treating universal quantifiers as the adversarial infimum of satisfaction probabilities, our framework enables the exact modeling of competitive interactions under uncertainty. 
Our approach leverages Cylindrical Algebraic Decomposition (CAD) to derive exact symbolic probability expressions for Nonlinear Real Arithmetic (NRA) formulas, moving beyond the limitations of linear constraints and point-value estimations. Central to our contribution is a recursive quantifier elimination algorithm designed to handle variable-dependent domains and non-algebraic expressions through a variable reparameterization technique. 
Experimental evaluation across baseline synthetic formulas, strategic economic models, and probabilistic program verification benchmarks demonstrates that our framework consistently computes exact symbolic solutions. By achieving a degree of symbolic precision and expressiveness unattainable by traditional numerical solvers, this work establishes a new baseline for exact reasoning in stochastic adversarial environments.

Cite As Get BibTex

Jung-Cheng Lin, Chia-Hsuan Su, Jie-Hong R. Jiang, and Hiroshi Unno. Exact Symbolic Reasoning for Nonlinear Stochastic SMT via Cylindrical Algebraic Decomposition. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.24

Author Details

Jung-Cheng Lin
  • Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
Chia-Hsuan Su
  • Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
Jie-Hong R. Jiang
  • Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan
  • Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
Hiroshi Unno
  • Research Institute of Electrical Communication, Tohoku University, Sendai, Japan

Funding

This work was supported in part by the National Science and Technology Council of Taiwan under Grant NSTC 114-2221-E-002-183-MY3, by National Taiwan University under Grant NTU-DE114FR032, and by JSPS KAKENHI of Japan under Grant JP25K24739.

Supplementary Materials

References

  1. S. Akshay, Supratik Chakraborty, Amir Kafshdar Goharshady, R. Govind, Harshit Jitendra Motwani, and Sai Teja Varanasi. Practical approximate quantifier elimination for non-linear real arithmetic. In André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods, pages 111-130, Cham, 2025. Springer Nature Switzerland. Google Scholar
  2. Saugata Basu. Algorithms in real algebraic geometry: A survey. In Karim Bekka, Goulwen Fichou, Jean-Philippe Monnier, and Ronan Quarez, editors, Real Algebraic Geometry, volume 51 of Panoramas et Synthèses, pages 107-153. Société Mathématique de France, 2017. URL: https://smf.emath.fr/node/44883.
  3. Nikolaj S Bjørner and Mikolás Janota. Playing with quantified satisfaction. LPAR (short papers), 35:15-27, 2015. URL: https://doi.org/10.29007/VV21.
  4. Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier. QSMA: a new algorithm for quantified satisfiability modulo theory and assignment. In International Conference on Automated Deduction, pages 78-95. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_5.
  5. Bob F. Caviness and Jeremy R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts & Monographs in Symbolic Computation. Springer Vienna, 1 edition, 1998. URL: https://doi.org/10.1007/978-3-7091-9459-1.
  6. George E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In H. Brakhage, editor, Automata Theory and Formal Languages, pages 134-183, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg. Google Scholar
  7. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  8. Martin Fränzle, Holger Hermanns, and Tino Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, pages 172-186, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-78929-1_13.
  9. Yang Gao and Martin Fränzle. A solving procedure for stochastic satisfiability modulo theories with continuous domain. In Javier Campos and Boudewijn R. Haverkort, editors, Quantitative Evaluation of Systems, pages 295-311, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-22264-6_19.
  10. Yang Gao and Martin Franzle. CSiSAT: A satisfiability solver for SMT formulas with continuous probability distributions. In 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR), pages 1-6, 2016. URL: https://doi.org/10.1109/SNR.2016.7479382.
  11. Jaakko Hintikka. Game-theoretical semantics: Insights and prospects. Notre Dame Journal of Formal Logic, 23(2):219-241, 1982. URL: https://doi.org/10.1305/ndjfl/1093883627.
  12. Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, and Joost-Pieter Katoen. Exact bayesian inference for loopy probabilistic programs using generating functions. Proc. ACM Program. Lang., 8(OOPSLA1), 2024. URL: https://doi.org/10.1145/3649844.
  13. Donald E. Knuth. Two notes on notation. The American Mathematical Monthly, 99(5):403-422, 1992. URL: http://www.jstor.org/stable/2325085.
  14. Michael L. Littman, Stephen M. Majercik, and Toniann Pitassi. Stochastic Boolean satisfiability. Journal of Automated Reasoning, 27(3):251-296, 2001. URL: https://doi.org/10.1023/A:1017584715408.
  15. Wolfram Alpha LLC. Wolfram|Alpha. https://www.wolframalpha.com/, 2026. Accessed: 2026-02-04.
  16. Aaron Meurer, Christopher Smith, Mateusz Paprocki, Ondřej Čertík, Sergey Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian Granger, Richard Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, and Anthony Scopatz. SymPy: Symbolic computing in python, June 2016. URL: https://doi.org/10.7287/peerj.preprints.2083.
  17. Marcel Moosbrugger. Automated analysis of probabilistic loops. PhD thesis, Technische Universität Wien, 2024. Google Scholar
  18. Marcel Moosbrugger, Julian Müllner, Ezio Bartocci, and Laura Kovács. Polar: An Algebraic Analyzer for (Probabilistic) Loops, pages 179-200. Springer Nature Switzerland, November 2024. URL: https://doi.org/10.1007/978-3-031-75783-9_8.
  19. Charlie Murphy and Zachary Kincaid. Quantified linear arithmetic satisfiability via fine-grained strategy improvement. In International Conference on Computer Aided Verification, pages 89-109. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_5.
  20. Christos H. Papadimitriou. Games against nature. Journal of Computer and System Sciences, 31(2):288-301, 1985. URL: https://doi.org/10.1016/0022-0000(85)90045-5.
  21. ProbInG Lab, TU Wien. Probing benchmark suite for probabilistic program analysis, 2024. Online; accessed 9 March 2026. URL: https://probing-lab.github.io/benchmarks/.
  22. Markus Schweighofer. Real algebraic geometry, positivity and convexity. arXiv preprint arXiv:2205.04211, 2022. URL: https://doi.org/10.48550/arXiv.2205.04211.
  23. Tino Teige and Martin Fränzle. Stochastic satisfiability modulo theories for non-linear arithmetic. In Laurent Perron and Michael A. Trick, editors, Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pages 248-262, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-68155-7_20.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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