Edinburgh Research Explorer

A Comparison of Decision Procedures in Presburger Arithmetic

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

Original languageEnglish
Title of host publicationProceedings of the VIII Conference on Logic and Computer Science (LIRA 97)
Number of pages6
StatePublished - 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
CountrySerbia
CityNovi Sad
Period1/09/974/09/97

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

Download statistics

No data available

ID: 27376251