Efficient Volume Computation for SMT Formulas

TL;DR

This paper presents ttc, an efficient algorithm that extends SMT solvers to compute the volume of satisfiable regions in Linear Real Arithmetic formulas, with significant performance improvements demonstrated through experiments.

Contribution

Introduction of ttc, a novel algorithm that combines set union, volume computation, and AllSAT techniques to efficiently calculate volumes in SMT formulas.

Findings

Significant performance improvements over existing methods

Effective decomposition of solution space into convex polytopes

Successful application to quantitative verification problems

Abstract

Satisfiability Modulo Theory (SMT) has recently emerged as a powerful tool for solving various automated reasoning problems across diverse domains. Unlike traditional satisfiability methods confined to Boolean variables, SMT can reason on real-life variables like bitvectors, integers, and reals. A natural extension in this context is to ask quantitative questions. One such query in the SMT theory of Linear Real Arithmetic (LRA) is computing the volume of the entire satisfiable region defined by SMT formulas. This problem is important in solving different quantitative verification queries in software verification, cyber-physical systems, and neural networks, to mention a few. We introduce ttc, an efficient algorithm that extends the capabilities of SMT solvers to volume computation. Our method decomposes the solution space of SMT Linear Real Arithmetic formulas into a union of overlapping convex polytopes, then computes their volumes and calculates their union. Our algorithm builds on recent developments in streaming-mode set unions, volume computation algorithms, and AllSAT techniques. Experimental evaluations demonstrate significant performance improvements over existing state-of-the-art approaches.