(Yet another) decision procedure for Equality LogicEquality LogicSlide 3Basic notionsFrom Equality to Propositional Logic Bryant & Velev CAV’00 – the Sparse methodSlide 6Slide 7Slide 8Slide 9Slide 10Slide 11An improvement Reduced Transitivity Constraints (RTC)Monotonicity of NNFSlide 14Slide 17Slide 18DefinitionsMain theoremProof of the main theoremDefinitions for the proof…More definitions for the proof…Slide 25Proof…ReConstructing SSlide 28Slide 29Slide 30Applying RTCSlide 33Slide 34Slide 35Constrains all contradictory cyclesConstraining simple contradictory cyclesSlide 38ResultsExample: Circuit TransformationsSlide 41Validating Circuit TransformationsValidating a compilation processSlide 44Slide 45Technion 1(Yet another) decision procedure for Equality LogicOfer Strichman and Orly MeirTechnionTechnion 2Equality Logic E: (x1 = x2 Æ (x2  x3 Ç x1  x3)) Domain: x1,x2,x3 2 NThe satisfiability problem: is there an assignment to x1,x2,x3 that satisfies E ?Q: When is Equality Logic useful ?...0 0 0 01 1Technion 3Equality LogicE: (x1 = x2 Æ (x2  x3 Ç x1  x3)) A: Mainly when combined with Uninterpreted Functions f (x,y), g(z),…Mainly used in proving equivalences, but not only.0 0 0 01 1Technion 4Basic notionsE: x = y Æ y = z Æ z  xxyz(non-polar) Equality Graph:Gives an abstract view of ETechnion 5From Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodE : x1 = x2 Æ x2 = x3 Æ x1  x3 B : e1,2Æ e2,3 Æ :e1,3Encode all edges with Boolean variablesThis is an abstractionTransitivity of equality is lost!Must add transitivity constraints!e1,3e1,2e2,3x1x2x3Technion 6From Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodE : x1 = x2 Æ x2 = x3 Æ x1  x3 B : e1,2Æ e2,3 Æ :e1,3Transitivity Constraints: For each cycle of size n, forbid a true assignment to n-1 edges T S = (e1,2 Æ e2,3 ! e1,3) Æ (e1,2 Æ e1,3 ! e2,3) Æ (e1,3 Æ e2,3 ! e1,2)Check: B Æ T Se1,3e1,2e2,3x1x2x3Technion 7Thm-1: It is sufficient to constrain simple cycles onlye1e2e3e4e5e6TT TTTFFrom Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodTechnion 8Thm-2: It is sufficient to constrain chord-free simple cyclese1e2e3e4e5TTTFTFFrom Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodTechnion 9Still, there can be an exponential number of chord-free simple cycles…Solution: make the graph ‘chordal’!….From Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodTechnion 10Dfn: A graph is chordal iff every cycle of size 4 or more has a chord.How to make a graph chordal ? eliminate vertices one at a time, and connect their neighbors. From Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodTechnion 11In a chordal graph, it is sufficient to constrain only triangles.Polynomial # of edges and constraints.# constraints = 3 £ #trianglesTTTTFTTContradiction!From Equality to Propositional LogicBryant & Velev CAV’00 – the Sparse methodTechnion 12An improvementReduced Transitivity Constraints (RTC)So far we did not consider the polarity of the edges. Assuming E is in Negation Normal Form E: x = y Æ y = z Æ z  xxyz(polar) Equality Graph:==Technion 13Monotonicity of NNFThm-3: NNF formulas are monotonically satisfied(in CNF this is simply the pure literal rule)Let  be in NNF and satisfiable. Thm-3 implies: Let  ² Derive ’ from  by switching the value of a ‘mis-assigned’ pure literal in  Now ’ ² Technion 14Claim: in the following graph T R = e3 Æ e2 ! e1 is sufficientThis is only true because of monotonicity of NNF (an extension of the pure literal rule)An improvementReduced Transitivity Constraints (RTC)e1e2e3xzy==Allowing e.g. e1 = e2 = T, e3= FTechnion 17Basic notions Equality Path: a path made of equalities. we write x =*zDisequality Path: a path made of equalities and exactly one disequality. We write x *yContradictory Cycle: two nodes x and y, s.t. x=*y and x * y form a contradictory cyclexyzTechnion 18Basic notions Thm-4: Every contradictory cycle is either simple or contains a simple contradictory cycleTechnion 19DefinitionsDfn: A contradictory Cycle C is constrained under T if T does not allow this assignment C =FTTTTTechnion 21Main theoremIf T R constrains all simple contradictory cycles, andFor every assignment S, S ² T S ! S ² T Rthen E is satisfiable iff B Æ T R is satisfiableThe Equality FormulaFrom the Sparse methodTechnion 22Proof of the main theorem() E is satisfiable  B T ÆS is satisfiable  B T ÆR is satisfiable() Proof strategy: Let R be a satisfying assignment to B Æ T R We will construct S that satisfies B Æ T SFrom this we will conclude that E is satisfiableSkip proofTechnion 23Definitions for the proof…A Violating cycle under an assignment RThis assignment violates T S but not necessarily T ReFeT2eT1TTFEither dashed or solidTechnion 24More definitions for the proof…An edge e = (vi,vj) is equal under an assignment  iff there is an equality path between vi and vj all assigned T under Denote: TTFTTv1v2v3Technion 25More definitions for the proof…An edge e = (vi,vj) is disequal under an assignment  iff there is a disequality path between vi and vj in which the solid edge is the only one assigned false by Denote: TTFTTv1v2v3Technion 26Proof…Observation 1: The combinationis impossible if = R(recall: R ² T R)Observation 2: if (v1,v3) is solid, thenFTTv1v2v3Technion 27ReConstructing SType 1:It is not the case that Assign S (e23) = FType 2: Otherwise it is not the case that  Assign  (e13) = TFTTIn all other cases S = RFTT F Tv1v2v3v1v2v3Technion 28ReConstructing SStarting from R, repeat until convergence: (eT) := F in all Type 1 cycles (eF) := T in all Type 2 cyclesAll Type 1 and Type 2 triangles now satisfy T S B is still satisfied (monotonicity of NNF)Left to prove: all contradictory cycles are still satisfiedTechnion 29Proof…Invariant: contradictory cycles are not violating throughout the reconstruction. contradicts the precondition to make this assignment…FTTv1v2v3 FTTTechnion 30Proof…Invariant: contradictory