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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 64–78. Springer, Heidelberg (2000)
Cormen, T.T., Leiserson, C.E., Rivest, R.L.: Introduction to algorithms. MIT Press, Cambridge (1990)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. of the ACM 5(7), 394–397 (1962)
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)
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)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)
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)
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)
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)
Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, Springer, Heidelberg (1997)
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)
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)
Nelson, G., Oppen, D.C.: Fast decision procedures bases on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)
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)
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)
Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACMÂ 21(7) (1978)
Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. Journal of the ACM (JACM) 22(2), 215–225 (1975)
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)
Tiwari, A., Vigneron, L.: Implementation of Abstract Congruence Closure with randomly generated CC problem instances (2001), At http://www.csl.sri.com/users/tiwari
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nieuwenhuis, R., Oliveras, A. (2005). Proof-Producing Congruence Closure. In: Giesl, J. (eds) Term Rewriting and Applications. RTA 2005. Lecture Notes in Computer Science, vol 3467. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32033-3_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-32033-3_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25596-3
Online ISBN: 978-3-540-32033-3
eBook Packages: Computer ScienceComputer Science (R0)