Publication Details
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Hečko Michal, Ing. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Habermehl Peter
Presburger arithmetic, linear integer arithmetic, SMT solver, automata-logic
connection
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.
@inproceedings{BUT188628,
author="Vojtěch {Havlena} and Michal {Hečko} and Lukáš {Holík} and Ondřej {Lengál} and Peter {Habermehl}",
title="Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic",
booktitle="Proceedings of CAV'24",
year="2024",
journal="Lecture Notes in Computer Science",
number="14681",
pages="42--67",
publisher="Springer Verlag",
address="Montreal",
doi="10.1007/978-3-031-65627-9\{_}3",
issn="0302-9743"
}