## Paper: A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams (at LICS 2005)

**Jérôme Leroux**

### Abstract

Number Decision Diagrams (NDD) are the automatabased symbolic representation for manipulating sets of integer vectors encoded as strings of digit vectors (least or most significant digit first). Since 1969 [8, 29], we know that any Presburger-definable set [26] (a set of integer vectors satisfying a formula in the first-order additive theory of the integers) can be represented by a NDD, and efficient algorithm for manipulating these sets have been recently developed [31, 4]. However, the problem of deciding if a NDD represents such a set, is a well-known hard problem first solved by Muchnik in 1991 [23, 24, 5] with a quadruplyexponential time algorithm. In this paper, we show how to determine in polynomial time whether a NDD represents a Presburger-definable set, and we provide in this positive case a polynomial time algorithm that constructs from the NDD a Presburger-formula that defines the same set.

### BibTeX

@InProceedings{Leroux-APolynomialTimePres, author = {Jérôme Leroux}, title = {A Polynomial Time Presburger Criterion and Synthesis for Number Decision Diagrams}, booktitle = {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)}, year = {2005}, month = {June}, pages = {147--156}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }