SMT Sampling via Model-Guided Approximation
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.
Cite
@article{arxiv.2212.06472,
title = {SMT Sampling via Model-Guided Approximation},
author = {Matan Peled and Bat-Chen Rothenberg and Shachar Itzhaky},
journal= {arXiv preprint arXiv:2212.06472},
year = {2022}
}