SMT sampling via model-guided approximation

DOI10.1007/978-3-031-27481-7_6zbMath1529.68284arXiv2212.06472MaRDI QIDQ6174528

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

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

satisfiability modulo theoriesunder-approximationmodel-guided approximationSMT sampling

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)

Cites Work

• Unnamed Item
• SMT-based model checking for recursive programs
• Fast sampling of perfectly uniform satisfying assignments
• Generating Diverse Solutions in SAT
• Importance Sampling for Stochastic Simulations
• Discrete Hit-and-Run for Sampling Points from Arbitrary Distributions Over Subsets of Integer Hyperrectangles
• Proving Termination Through Conditional Termination
• Knowledge Compilation meets Uniform Sampling
• The MathSAT5 SMT Solver
• Monte Carlo sampling methods using Markov chains and their applications
• Deciding Bit-Vector Arithmetic with Abstraction
• Quantum rejection sampling

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