Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)

Peter Habermehl, Vojtěch Havlena, Michal Hečko, Lukáš Holík, Ondřej Lengál

TL;DR

The paper tackles the challenge of solving quantified linear integer arithmetic (Presburger arithmetic), where SMT solvers struggle with quantifiers. It introduces a hybrid approach that blends automata-based bitvector reasoning with algebraic optimizations, leveraging a fine-grained duality between automata and arithmetic formulae via derivatives to generate and prune states on the fly. The principal contributions are the derivative-based automaton construction, a suite of algebraic rewrites and pruning techniques (including simplifications, disjunction pruning, Cooperenstein-like instantiations and Omega-test-inspired strategies), and a proof-of-concept implementation that competes with state-of-the-art SMT solvers, often excelling on quantifier-heavy instances. This work demonstrates that exploiting the automata-algebraic interface can substantially improve LIA reasoning in SMT contexts and points to further integration opportunities with existing solvers.

Abstract

We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (nowadays prevalent) algebraic approaches, which work directly with numbers. This combination is enabled by a fine-grained version of the duality between automata and arithmetic formulae. In particular, we employ a construction where states of automaton are obtained as derivatives of arithmetic formulae: then every state corresponds to a formula. Optimizations based on techniques and ideas transferred from the world of algebraic methods are used on thousands of automata states, which dramatically amplifies their effect. The merit of this combination of automata with algebraic methods is demonstrated by our prototype implementation being competitive to and even superior to state-of-the-art SMT solvers.

Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)

TL;DR

The paper tackles the challenge of solving quantified linear integer arithmetic (Presburger arithmetic), where SMT solvers struggle with quantifiers. It introduces a hybrid approach that blends automata-based bitvector reasoning with algebraic optimizations, leveraging a fine-grained duality between automata and arithmetic formulae via derivatives to generate and prune states on the fly. The principal contributions are the derivative-based automaton construction, a suite of algebraic rewrites and pruning techniques (including simplifications, disjunction pruning, Cooperenstein-like instantiations and Omega-test-inspired strategies), and a proof-of-concept implementation that competes with state-of-the-art SMT solvers, often excelling on quantifier-heavy instances. This work demonstrates that exploiting the automata-algebraic interface can substantially improve LIA reasoning in SMT contexts and points to further integration opportunities with existing solvers.

Abstract

We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (nowadays prevalent) algebraic approaches, which work directly with numbers. This combination is enabled by a fine-grained version of the duality between automata and arithmetic formulae. In particular, we employ a construction where states of automaton are obtained as derivatives of arithmetic formulae: then every state corresponds to a formula. Optimizations based on techniques and ideas transferred from the world of algebraic methods are used on thousands of automata states, which dramatically amplifies their effect. The merit of this combination of automata with algebraic methods is demonstrated by our prototype implementation being competitive to and even superior to state-of-the-art SMT solvers.
Paper Structure (6 sections, 1 theorem, 6 equations, 3 figures)

This paper contains 6 sections, 1 theorem, 6 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Finite automata.
  4. Linear integer arithmetic.
  5. Classical Automata-Based Decision Procedure for LIA
  6. Base case.

Key Result

lemma thmcounterlemma

$\mathit{Reach}(\{\begin{tikzpicture}[anchor=base,baseline]{ \node[inner sep=0.5mm, fill=blue!5, minimum height=4mm] {$\varphi_{\mathit{atom}}$};}\end{tikzpicture}\}, \Sigma_{\mathbb{X}})$ is finite for an atomic formula \begin{tikzpicture}[anchor=base,baseline]{ \node[inner sep=0.5mm, fill=blue

Figures (3)

  • Figure 1: Comparison of the peak intermediate automaton size and the size of the minimized DFA for the entire formula on the SMT-COMP benchmark (cf. \ref{['sec:experiments']}).
  • Figure 2: Definition of the transition function $\mathit{Post}$ for atomic formulae. Note that the right-hand sides contain constant expressions, so they will be evaluated.
  • Figure 3: Acceptance for atomic formulae.

Theorems & Definitions (2)

  • lemma thmcounterlemma
  • proof