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)
ER -