SMT Sampling via Model-Guided Approximation

TL;DR

This paper introduces a new efficient method for generating multiple satisfying assignments in SMT formulas involving integer arithmetic, arrays, and uninterpreted functions, by reducing the sampling problem to independent interval sampling.

Contribution

It presents a novel model-guided approximation approach for SMT sampling that extends to theories with arrays and uninterpreted functions, improving sampling efficiency.

Findings

Effective reduction of SMT sampling to independent interval sampling.

Applicable to theories involving integers, arrays, and uninterpreted functions.

Enhances the generation of multiple SMT solutions for verification tasks.

Abstract

We investigate the domain of satisfiable formulas in satisfiability modulo theories (SMT), in particular, automatic generation of a multitude of satisfying assignments to such formulas. Despite the long and successful history of SMT in model checking and formal verification, this aspect is relatively under-explored. Prior work exists for generating such assignments, or samples, for Boolean formulas and for quantifier-free first-order formulas involving bit-vectors, arrays, and uninterpreted functions (QF_AUFBV). We propose a new approach that is suitable for a theory T of integer arithmetic and to T with arrays and uninterpreted functions. The approach involves reducing the general sampling problem to a simpler instance of sampling from a set of independent intervals, which can be done efficiently. Such reduction is carried out by expanding a single model - a seed - using top-down propagation of constraints along the original first-order formula.