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

TL;DR

This paper introduces a novel approach to solving quantified linear integer arithmetic by integrating automata-based methods with algebraic techniques, leveraging a duality between automata and formulas, resulting in a competitive solver.

Contribution

It presents a new hybrid method combining automata and algebraic approaches for linear integer arithmetic, with a derivative-based automaton state construction and optimizations that outperform existing SMT solvers.

Findings

Prototype implementation is competitive with state-of-the-art SMT solvers.

Automata states derived as derivatives of formulas improve efficiency.

Algebraic optimizations significantly enhance automata-based reasoning.

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.