Advertisement

Proof-Producing Congruence Closure

  • Robert Nieuwenhuis
  • Albert Oliveras
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)

Abstract

Many applications of congruence closure nowadays require the ability of recovering, among the thousands of input equations, the small subset that caused the equivalence of a given pair of terms. For this purpose, here we introduce an incremental congruence closure algorithm that has an additional \(\mathit{Explain}\) operation.

First, two variations of union-find data structures with \(\mathit{Explain}\) are introduced. Then, these are applied inside a congruence closure algorithm with \(\mathit{Explain}\), where a k-step proof can be recovered in almost optimal time (quasi-linear in k), without increasing the overall O(n log n) runtime of the fastest known congruence closure algorithms.

This non-trivial (ground) equational reasoning result has been quite intensively sought after (see, e.g., [SD99,dMRS04,KS04]), and moreover has important applications to verification.

Keywords

Decision Procedure Recursive Call Congruence Relation Proof Tree Union Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [ABC+02]
    Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 195–210. Springer, Heidelberg (2002)Google Scholar
  2. [BDS02]
    Barrett, C., Dill, D., Stump, A.: Checking satisfiability of first-order formulas by incremental translation into sat. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 236. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. [BT00]
    Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 64–78. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. [CLR90]
    Cormen, T.T., Leiserson, C.E., Rivest, R.L.: Introduction to algorithms. MIT Press, Cambridge (1990)zbMATHGoogle Scholar
  5. [DLL62]
    Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. of the ACM 5(7), 394–397 (1962)zbMATHCrossRefMathSciNetGoogle Scholar
  6. [dMR02]
    de Moura, L., Rueß, H.: Lemmas on demand for satisfiability solvers. In: Procs. 5th Int. Symp. on the Theory and Applications of Satisfiability Testing, SAT 2002, pp. 244–251 (2002)Google Scholar
  7. [dMRS04]
    de Moura, L., Rueß, H., Shankar, N.: Justifying equality. In: Proc. of the Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning, Cork, Ireland (2004)Google Scholar
  8. [DP60]
    Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)zbMATHCrossRefMathSciNetGoogle Scholar
  9. [DST80]
    Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. of the Association for Computing Machinery 27(4), 758–771 (1980)zbMATHMathSciNetGoogle Scholar
  10. [FJOS03]
    Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explanation. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. [GHN+04]
    Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. [Kap97]
    Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, Springer, Heidelberg (1997)Google Scholar
  13. [KS04]
    Klapper, R., Stump, A.: Validated proof-producing decision procedures. In: Proceedings of the Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning, Cork, Ireland (2004)Google Scholar
  14. [MMZ+01]
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. 38th Design Automation Conference, DAC 2001 (2001)Google Scholar
  15. [NO80]
    Nelson, G., Oppen, D.C.: Fast decision procedures bases on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)zbMATHMathSciNetGoogle Scholar
  16. [NO03]
    Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 78–90. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. [SD99]
    Stump, A., Dill, D.L.: Generating proofs from a decision procedure. In: Pnueli, A., Traverso, P. (eds.) Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy (1999)Google Scholar
  18. [Sho78]
    Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7) (1978)Google Scholar
  19. [Tar75]
    Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. Journal of the ACM (JACM) 22(2), 215–225 (1975)zbMATHCrossRefMathSciNetGoogle Scholar
  20. [Tar79]
    Tarjan, R.E.: A class of algorithms that require nonlinear time to maintain disjoint sets. J. Comput. and Sys. Sci. 18(2), 110–127 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  21. [TV01]
    Tiwari, A., Vigneron, L.: Implementation of Abstract Congruence Closure with randomly generated CC problem instances (2001), At http://www.csl.sri.com/users/tiwari

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Robert Nieuwenhuis
    • 1
  • Albert Oliveras
    • 1
  1. 1.Technical University of CataloniaBarcelonaSpain

Personalised recommendations