A Comparison of Decision Procedures in Presburger Arithmetic

Predrag Janicic, Ian Green, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

It is part of the tradition and folklore of automated reasoning that the intractability of Coopers decision procedure for Presburger integer arithmetic makes is too expensive for practical use. More than years of work has resulted in numerous approximate procedures via rational arithmetic all of which are incomplete and restricted to the quantierfree fragment. In this paper we report on an experiment which strongly questions this tradition We measured the performance of procedures due to Hodes Cooper and heuristic variants thereof which detect counter examples across acorpus of randomly generated quantier free Presburger formulae. The results are startling a variant of Coopers procedure outperforms Hodes procedure on both valid and invalid formulae and is fast enough for practical use. These results contradict much perceived wisdom that decision procedures for integer arithmetic are too expensive to use in practice
Original languageEnglish
Title of host publicationProceedings of the VIII Conference on Logic and Computer Science (LIRA 97)
Number of pages6
Publication statusPublished - 1997
EventVIII International Conference on Logic and Computer Science - Theoretical Foundations of Computing - Novi Sad, Serbia
Duration: 1 Sep 19974 Sep 1997

Conference

ConferenceVIII International Conference on Logic and Computer Science - Theoretical Foundations of Computing
Country/TerritorySerbia
CityNovi Sad
Period1/09/974/09/97

Fingerprint

Dive into the research topics of 'A Comparison of Decision Procedures in Presburger Arithmetic'. Together they form a unique fingerprint.

Cite this