An Automata-Theoretic Algorithm for Counting Solutions to Presburger Formulas

We present an algorithm for counting the number of integer solutions to selected free variables of a Presburger formula. We represent the Presburger formula as a deterministic finite automaton (DFA) whose accepting paths encode the standard binary representations of satisfying free variable values. We count the number of accepting paths in such a DFA to obtain the number of solutions without enumerating the actual solutions. We demonstrate our algorithm on a suite of eight problems to show that it is universal, robust, fast, and scalable.

• Type: Conference
• Year: 2004
• Where: CC
• Authors: Erin Parker, Siddhartha Chatterjee
• Keywords: CC 2004, Deterministic finite Automaton, Free Variable, Presburger Formula, Programming Languages