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 piecewise-polynomial solutions. By providing a level of symbolic precision and expressiveness unattainable by traditional numerical solvers, this work establishes a new baseline for exact reasoning in stochastic adversarial environments.

ABSTRACT. In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries. In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. We have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the feasibility and the effectiveness of the approach.

ABSTRACT. The theory of uninterpreted functions is a key modeling tool for systems with unknown or abstracted components. Some domains such as systems biology impose further restrictions regarding monotonicity on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand. We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.