一句话：提出全自动方法计算 Presburger 算术公式最小 DFA 规模的下界，并生成可独立验证且可合并的证书。
该文关注逻辑理论中计算资源下界难以估计的问题，目标是给出编码 Presburger 算术（线性整数算术）公式解集的最小确定性有限自动机（DFA）规模的下界。作者提出一种全自动方法，生成可独立验证的证书，并支持类似并集的操作以逐步提高下界。基于 SMT-LIB 中超过 5000 个无量词 Presburger 公式进行大规模评估，结果显示所得下界常接近实际最小 DFA 规模；即使现有基于自动机的 Presburger 求解工具因规模过大而无法处理（相差数个数量级）的实例，该方法也能算出非平凡下界。
Lower bounds provide essential insights into the minimal computational resources required for algorithm execution. This paper focuses on logical theories, a domain where estimating resources is particularly difficult, and provides a novel, fully-automated method for computing lower bounds on memory usage, serving as a proxy for the computational resources required to perform logical reasoning. Specifically, the paper focuses on computing lower bounds on the size of the minimal deterministic finite automaton that encodes the solution set of a given Presburger arithmetic (also known as linear integer arithmetic) formula. The lower bounds are accompanied by independently verifiable certificates which also support a union-like operation that can be used to increase the computed bounds.We conducted an extensive empirical evaluation of our method using over 5 000 formulae from the quantifier-free fragment of Presburger arithmetic, sourced from the SMT-LIB repository. The results show that our method often produces lower bounds that are close to the actual size of the minimal deterministic finite automaton. Moreover, it succeeds in computing non-trivial bounds even for instances that are out of reach (by several orders of magnitude) for the existing state-of-the-art automata-based tools for solving Presburger arithmetic.
DOI 原文 ·
@inproceedings{paperbot9221,
title = {How Big is the Automaton? Certified Lower Bounds on the Size of Presburger DFAs},
author = {Nicolas Amat and Pierre Ganty and Alessio Mansutti},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00219}
}