M.Sc Student | Meir Orly |
---|---|

Subject | A Decision Procedure for Equality Logic |

Department | Department of Computer Science |

Supervisor | Professor Ofer Strichman |

We introduce a new decision procedure for deciding Equality
Logic, a logic fragment frequently used in verification of infinite-state systems. The procedure improves on Bryant and Velev's SPARSE method suggested in CAV 2000, in which each equality predicate is encoded with a Boolean variable, and then a set of transitivity constraints are added to compensate for the lost 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 is in Negation Normal Form (NNF). Given this information, we build the Equality Graph corresponding to
the Equality Logic formula 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 SPARSE method.

RTC is a polynomial algorithm which finds these necessary transitivity constraints. 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.