Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #872
Title:	A Comparison of Decision Procedures in Presburger Arithmetic
Authors:	Janicic,P; Green,I; Bundy,A
Date:	Oct 1997
Presented:	To be presented at Logic and Computer Science, Novi Sud, Yugoslavia, 1997
Keywords:
Abstract:	It is part of the tradition and folklore of automated reasoning that the intractability od Cooper's decision procedure for Presburger integer arithmetic makes it too expensive for practical use. More than 25 years of work has resulted in numerous approximate procedures via rational arithmetic, all of which are incomplete and restricted to the quantifier-free fragment (for example, Hodes' procedure in Nqthm). In this paper we report on an experiment which assesses this tradition. We measured the performance of procedures due to Hodes, Cooper (and heuristic variants thereof which detect counterexamples), across two copora of quantifier-free Presburger formulae, one arising from inductive verification proofs, and another of 10 000 randomly generated formulae. the results on the inductive corpus expose the incompleteness of Hodes' procedure and show it to be slower than Cooper's. On the random corpus, the results are similar; furthermore, a variant of Cooper's procedure significantly outperforms Hodes'. These results do not support much received wisdom concerning decision procedures for integer arithmetic, and at least suggest a reappraisal of the role of Cooper's procedure.
Download:	POSTSCRIPT COPY

Division of InformaticsForrest Hill & 80 South Bridge