Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic

AbstractIn a CAV'05 paper [Meir, O. and O. Strichman, Yet another decision procedure for equality logic, in: K. Etessami and S. Rajamani, editors, Proc. 17th Intl. Conference on Computer Aided Verification (CAV'05), Lect. Notes in Comp. Sci. 3576 (2005), pp. 307–320] we introduced a new decision procedure for Equality Logic: 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. The constraints are derived by analyzing Contradictory Cycles: cycles in the equality graph with exactly one disequality. Such a cycle is called constrained under a formula ϕ if ϕ is not satisfied with an assignment of true to all equality edges and false to the disequality edge. While we proved in [Meir, O. and O. Strichman, Yet another decision procedure for equality logic, in: K. Etessami and S. Rajamani, editors, Proc. 17th Intl. Conference on Computer Aided Verification (CAV'05), Lect. Notes in Comp. Sci. 3576 (2005), pp. 307–320] that it is sufficient to constrain all simple contradictory cycles, we left open the question of how to find the necessary constraints in polynomial time. Instead, we showed two possible compromises: an exponential algorithm, or, alternatively, a polynomial approximation that constrains all contradictory cycles rather than only the simple ones. In this article we show a polynomial algorithm that constrains only the simple contradictory cycles