Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theories Problems

Craig interpolation is used in solving bounded model checking (BMC) SAT and SMT problems.

In 2012, Teige et al. succeeded to compute interpolants for stochastic boolean satisfiability problems, i.e. SSAT.

That was achieved by defining sound and complete resolution calculus for SSAT and computing the Craig interpolation for A and B and not S_{A,B}, where not S_{A,B} represents a conflict clause of A and B. Consequently, one can obtain two interpolants for the formula Phi: A and B, where one interpolates A, and the second one interpolates B.

As a result of that, an approach to solve efficiently stochastic bounded model checker problems, e.g. MDPs, was addressed by using SSAT interpolation.

In this work we present a notion of Craig Interpolation for the stochastic modulo theories framework i.e. SSMT.

An SSMT formula consists of free and quantified variables where the latter variables are bound to discrete domains by existential or randomized quantifiers.

In the case of a randomized variable, the variable can be assigned to one of its domain values with a certain probability, where the summation of all probabilities of the same variable has to be one.

The significance of SSMT comes from the fact that one can encode probabilistic hybrid automata problems as SSMT formulae.

Our approach to compute the Craig interpolation for SSMT is as follows: we assume that arithmetic constraints can be relaxed as simple bounds by using interval constraint propagation (ICP) as implemented in iSAT tool. After that, we define a sound and relatively-complete resolution calculus for SSMT formula as done in case of SSAT, such that if a conflict clause is derived with a certain probability, then the latter probability is a safe upper bound of the real satisfaction probability of the SSMT formula. Then we extend P'udlak rules in a way such that simple bounds are treated as literals and if a conflict clause is derived, then we get a generalized Craig interpolation for the whole formula A and B and not S_{A,B}.

Finally, we adapt BMC to the probabilistic case, i.e. PBMC by encoding a step-bounded reachability problems as an SSMT formula, where a generalized Craig interpolation is used to compute an upper bound of the maximum probability of reaching the target states.