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

Authors: 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}
  }