SMT sampling via model-guided approximation

DOI10.1007/978-3-031-27481-7_6MaRDI QIDQ6174528zbMATH OpenFDO

Authors Matan I. Peled, Bat-Chen Rothenberg, Shachar Itzhaky

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2212.06472

zbMATH Keywords

model-guided approximationsatisfiability modulo theoriesSMT samplingunder-approximation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Recommendations

• Satisfiability modulo theories
• A survey of satisfiability modulo theory
• Approximate Counting in SMT and Value Estimation for Probabilistic Programs
• Approximate counting in SMT and value estimation for probabilistic programs
• Fast sampling of perfectly uniform satisfying assignments

Cites work

• Deciding Bit-Vector Arithmetic with Abstraction
• Discrete hit-and-run for sampling points from arbitrary distributions over subsets of integer hyperrectangles
• Fast sampling of perfectly uniform satisfying assignments
• Generating Diverse Solutions in SAT
• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• Importance Sampling for Stochastic Simulations
• Knowledge compilation meets uniform sampling
• Monte Carlo sampling methods using Markov chains and their applications
• Proving termination through conditional termination
• SMT-based model checking for recursive programs
• The MathSAT5 SMT solver

Cited in

(1)

• CSB: a counting and sampling tool for bit-vectors

This page was built for publication: SMT sampling via model-guided approximation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174528)