Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

Stefan Ratschan, Anggha Nugraha, Mikoláš Janota, Marek Dančo

TL;DR

This work introduces an alternative approach that certifies satisfiability using induction arguments, and applies it to the case of linear integer arithmetic, and is able to prove satisfiability of formulas that are out of reach for current SMT solvers.

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.

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

TL;DR

This work introduces an alternative approach that certifies satisfiability using induction arguments, and applies it to the case of linear integer arithmetic, and is able to prove satisfiability of formulas that are out of reach for current SMT solvers.

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.
Paper Structure (14 sections, 4 theorems, 25 equations, 1 figure, 1 algorithm)

This paper contains 14 sections, 4 theorems, 25 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Model-based and instantiation methods.
  4. Decision procedures for arrays and quantified formulas.
  5. Synthesis.
  6. Proof certificates and model representation.
  7. Problem Statement
  8. Notation and Terminology
  9. Satisfiability Certificates
  10. Algorithm
  11. Propositional Encoding
  12. Experiments
  13. Conclusion
  14. Appendix

Key Result

theorem 1

Every formula $\phi$ of the form $F\wedge \forall \bar{x}\;.\; Q$ that has a satisfiability certificate is satisfiable.

Figures (1)

  • Figure 1: Problems solved with increasing $c$. $*$ refers to unbounded problems.

Theorems & Definitions (13)

  • definition 1: Cell
  • definition 2: Cell Interpretation
  • definition 3: Pre-satisfiability Certificate
  • definition 4: Relevant Cells
  • definition 5: Satisfiability Certificate
  • theorem 1
  • proof
  • definition 6: ReqPivot Condition
  • definition 7: Interval Extension Formulas
  • theorem 2: Interval Satisfiability
  • ...and 3 more