Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

TL;DR

This paper presents an inductive certification method for satisfiability involving universal quantifiers and uninterpreted functions, improving the ability to prove satisfiability in complex formulas, especially in linear integer arithmetic.

Contribution

It introduces an inductive approach to certify satisfiability, overcoming limitations of existing SMT solvers in handling certain formulas.

Findings

Successfully certifies satisfiability of complex formulas

Proves formulas beyond current SMT solver capabilities

Applicable to linear integer arithmetic

Abstract

The combination of uninterpreted function symbols and universal quantification occurs in many applications of automated reasoning, for example, due to their ability to reason about arrays. Yet the satisfiability of such formulas is, in general, undecidable. In practice, SMT solvers are often successful in the unsatisfiable case, using heuristics. However, in the satisfiable case, they rely on explicit model construction, which fails for formulas whose smallest model is not small enough. We introduce an alternative approach that certifies satisfiability using induction arguments, and apply it to the case of linear integer arithmetic. The resulting algorithm is able to prove satisfiability of formulas that are out of reach for current SMT solvers.