Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要