Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic

9 years 8 months ago
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 ...
Tino Teige, Martin Fränzle
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Authors Tino Teige, Martin Fränzle
Comments (0)