Abstract
We introduce a new decision procedure for Equality Logic. The procedure improves on Bryant and Velev’s sparse method [4] from CAV’00, in which each equality predicate is encoded with a Boolean variable, and then a set of transitivity constraints are added to compensate for the loss of transitivity of equality. We suggest the Reduced Transitivity Constraints (RTC) algorithm, that unlike the sparse method, considers the polarity of each equality predicate, i.e. whether it is an equality or disequality when the given equality formula ϕ E is in Negation Normal Form (NNF). Given this information, we build the Equality Graph corresponding to ϕ E with two types of edges, one for each polarity. We then define the notion of Contradictory Cycles to be cycles in that graph that the variables corresponding to their edges cannot be simultaneously satisfied due to transitivity of equality. We prove that it is sufficient to add transitivity constraints that only constrain Contradictory Cycles, which results in only a small subset of the constraints added by the Reconstruct-αsparse method. The formulas we generate are smaller and define a larger solution set, hence are expected to be easier to solve, as indeed our experiments show. Our new decision procedure is now implemented in the uclid verification system.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Ackermann, W.: Solvable cases of the Decision Problem. In: Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)
Bryant, R., German, S., Velev, M.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 470–482. Springer, Heidelberg (1999)
Bryant, R., German, S., Velev, M.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic 2(1), 1–41 (2001)
Bryant, R., Velev, M.: Boolean satisfiability with transitivity constraints. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 78. Springer, Heidelberg (2002)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Cormen, T., Leiserson, C., Rivest, R.: Introduction to Algorithms, ch. 26, p. 563. MIT Press, Cambridge (2000)
Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing cnf formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 423–429. Springer, Heidelberg (2005)
Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University (2004)
Meir, O., Strichman, O.: Yet another decision procedure for equality logic (full version) (2005) ie.technion.ac.il/~ofers/cav05_full.ps
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. Design Automation Conference, DAC 2001 (2001)
Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding equality formulas by small-domains instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 455–469. Springer, Heidelberg (1999)
Pnueli, A., Rodeh, Y., Strichman, O., Siegel, M.: The small model property: How small can it be? Information and computation 178(1), 279–293 (2002)
Pnueli, A., Siegel, M., Shtrichman, O.: Translation validation for synchronous languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 235–246. Springer, Heidelberg (1998)
Rodeh, Y., Shtrichman, O.: Finite instantiations in equivalence logic with uninterpreted functions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 144. Springer, Heidelberg (2001)
Shostak, R.: An algorithm for reasoning about equality. Communications of the ACM 21(7), 583–585 (1978)
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
Meir, O., Strichman, O. (2005). Yet Another Decision Procedure for Equality Logic. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_32
Download citation
DOI: https://doi.org/10.1007/11513988_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)