Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic

Abstract. The stochastic satisfiability modulo theories (SSMT) problem is a generalization of the SMT problem on existential and randomized (aka. stochastic) quantification over discrete variables of an SMT formula. This extension permits the concise description of diverse problems combining reasoning under uncertainty with data dependencies. Solving problems with various kinds of uncertainty has been extensively studied in Artificial Intelligence. Famous examples are stochastic satisfiability and stochastic constraint programming. In this paper, we extend the algorithm for SSMT for decidable theories presented in [FHT08] to non-linear arithmetic theories over the reals and integers which are in general undecidable. Therefore, we combine approaches from Constraint Programming, namely the iSAT algorithm tackling mixed Boolean and non-linear arithmetic constraint systems, and from Artificial Intelligence handling existential and randomized quantifiers. Furthermore, we evaluate our novel ...

• Type: Conference
• Year: 2008
• Where: CPAIOR
• Authors: Tino Teige, Martin Fränzle
• Keywords: Constraint Programming, CPAIOR 2008, Operations Research, Stochastic Satisfiability, Stochastic Satisfiability Modulo