Fast Decision Procedures Based on Congruence Closure

ABSTRACT

The notion of the congruence closure of a relation on a graph is defined and several algorithms for computing it are surveyed. A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality. A decision procedure is then given for the quantifier-free theory of LISP list structure based on the congruence closure algorithm. Both decision procedures determine the satisfiability of a conjunction of literals of length n in average time O(n log n) using the fastest known congruence closure algorithm. It is also shown that if the axiomatization of the theory of list structure is changed slightly, the problem of determining the satisfiability of a conjunction of literals becomes NP-complete. The decision procedures have been implemented in the authors' simplifier for the Stanford Pascal Verifier.

REFERENCES

• 1: ACKERMANN, W Solvable Cases of the Dectston Problem North-Holland, Amsterdam, 1954
• 2: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 3: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 4: Dexter Kozen, Complexity of finitely presented algebras, Proceedings of the ninth annual ACM symposium on Theory of computing, p.164-177, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803406]
• 5: NELSON, C G., AND OPP~N, D. C Fast decision procedures based on UNION and'FIND. Proc E,ghteenth Annual Symp on Foundauons of Comptr. Sct, Providence, R I., 1977 (This is an earher verston of the present paper.)
• 6: NELSON, C G., AND OPPEN, D. C Stmphfieation by cooperating dec,slon procedures To be pubhshed
• 7: Derek C. Oppen, Reasoning about recursively defined data structures, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.151-157, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512776]
• 8: Robert E. Shostak, An algorithm for reasoning about equality, Communications of the ACM, v.21 n.7, p.583-585, July 1978 [doi>10.1145/359545.359570]
• 9: Robert Endre Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM (JACM), v.22 n.2, p.215-225, April 1975 [doi>10.1145/321879.321884]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Theory, Verification