# SMT Sampling via Model-Guided Approximation

arXiv: https://arxiv.org/abs/2212.06472 · HTML: https://mlsanity.com/paper/2212.06472/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Dec 2022.

## Built on by (most cited first, 2 of 2)

- [SMT(LIA) Sampling with High Diversity](https://mlsanity.com/paper/2503.04782/) (2025)
- [CSB: A Counting and Sampling tool for Bit-vectors](https://mlsanity.com/paper/2607.04142/) (2026)

## Abstract (arXiv)

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.