A Comparison of Decision Procedures in Presburger Arithmetic

Predrag Janicic; Ian Green; Alan Bundy

A Comparison of Decision Procedures in Presburger Arithmetic

Predrag Janicic, Ian Green, Alan Bundy

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English
Title of host publication	Proceedings of the VIII Conference on Logic and Computer Science (LIRA 97)
Number of pages	6
Publication status	Published - 1997
Event	VIII International Conference on Logic and Computer Science - Theoretical Foundations of Computing - Novi Sad, Serbia Duration: 1 Sept 1997 → 4 Sept 1997

Conference

Conference	VIII International Conference on Logic and Computer Science - Theoretical Foundations of Computing
Country/Territory	Serbia
City	Novi Sad
Period	1/09/97 → 4/09/97

Access to Document

rp872Accepted author manuscript, 167 KB

Cite this

@inproceedings{b6a0174877884e97ba807dc04765a1c8,

title = "A Comparison of Decision Procedures in Presburger Arithmetic",

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",

author = "Predrag Janicic and Ian Green and Alan Bundy",

year = "1997",

language = "English",

booktitle = "Proceedings of the VIII Conference on Logic and Computer Science (LIRA 97)",

note = "VIII International Conference on Logic and Computer Science - Theoretical Foundations of Computing ; Conference date: 01-09-1997 Through 04-09-1997",

}

TY - GEN

T1 - A Comparison of Decision Procedures in Presburger Arithmetic

AU - Janicic, Predrag

AU - Green, Ian

AU - Bundy, Alan

PY - 1997

Y1 - 1997

N2 - 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

AB - 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

M3 - Conference contribution

BT - Proceedings of the VIII Conference on Logic and Computer Science (LIRA 97)

T2 - VIII International Conference on Logic and Computer Science - Theoretical Foundations of Computing

Y2 - 1 September 1997 through 4 September 1997

ER -

A Comparison of Decision Procedures in Presburger Arithmetic

Abstract

Conference

Access to Document

Fingerprint

Cite this