6 Combination of decision procedures (1185842), страница 5
Текст из файла (страница 5)
of F1 , F2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories21/44Nelson-Oppen Method for Convex TheoriesIGiven formula F in T1 ∪ T2 (T1 , T2 convex), want to decide if F issatisfiableIFirst, purify F into F1 and F2IRun decision procedures for T1 , T2 to decide sat. of F1 , F2IIf either is unsat, F is unsatisfiable. Why?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories21/44Nelson-Oppen Method for Convex TheoriesIGiven formula F in T1 ∪ T2 (T1 , T2 convex), want to decide if F issatisfiableIFirst, purify F into F1 and F2IRun decision procedures for T1 , T2 to decide sat.
of F1 , F2IIf either is unsat, F is unsatisfiable. Why?IBecause F is equisatisfiable to F1 ∧ F2 , which is unsatVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories21/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?INo because if F1 and F2 are individually satisfiable, F1 ∧ F2 does not haveto be satisfiableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?INo because if F1 and F2 are individually satisfiable, F1 ∧ F2 does not haveto be satisfiableIExample:x + y = 2 ∧ x = 1 ∧ f (x ) 6= f (y)|{z}{z}|TZVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringT=Lecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?INo because if F1 and F2 are individually satisfiable, F1 ∧ F2 does not haveto be satisfiableIExample:x + y = 2 ∧ x = 1 ∧ f (x ) 6= f (y)|{z}{z}|TZIT=Here, F1 and F2 are individually sat, but their combination is unsat b/cTZ implies x = yVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?INo because if F1 and F2 are individually satisfiable, F1 ∧ F2 does not haveto be satisfiableIExample:x + y = 2 ∧ x = 1 ∧ f (x ) 6= f (y)|{z}{z}|TZT=IHere, F1 and F2 are individually sat, but their combination is unsat b/cTZ implies x = yIIn the case where F1 and F2 are sat, theories have to exchange all impliedequalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?INo because if F1 and F2 are individually satisfiable, F1 ∧ F2 does not haveto be satisfiableIExample:x + y = 2 ∧ x = 1 ∧ f (x ) 6= f (y)|{z}{z}|TZT=IHere, F1 and F2 are individually sat, but their combination is unsat b/cTZ implies x = yIIn the case where F1 and F2 are sat, theories have to exchange all impliedequalitiesIWhy only equalities?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIIf both are SAT, does this mean F is sat?INo because if F1 and F2 are individually satisfiable, F1 ∧ F2 does not haveto be satisfiableIExample:x + y = 2 ∧ x = 1 ∧ f (x ) 6= f (y)|{z}{z}|TZT=IHere, F1 and F2 are individually sat, but their combination is unsat b/cTZ implies x = yIIn the case where F1 and F2 are sat, theories have to exchange all impliedequalitiesIWhy only equalities? b/c it is the only shared symbolVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories22/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1.
F1 ⇒ x = yVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1. F1 ⇒ x = y2. F2 ⇒ x = yVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1. F1 ⇒ x = y2. F2 ⇒ x = yIIf (1) holds but not (2), conjoin x = y with F2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1.
F1 ⇒ x = y2. F2 ⇒ x = yIIf (1) holds but not (2), conjoin x = y with F2IIf (2) holds but not (1), conjoin x = y with F1Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1. F1 ⇒ x = y2. F2 ⇒ x = yIIf (1) holds but not (2), conjoin x = y with F2IIf (2) holds but not (1), conjoin x = y with F1ILet F10 and F20 denote new formulasVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1.
F1 ⇒ x = y2. F2 ⇒ x = yIIf (1) holds but not (2), conjoin x = y with F2IIf (2) holds but not (1), conjoin x = y with F1ILet F10 and F20 denote new formulasICheck satisfiability of F10 and F20Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44Nelson-Oppen Method for Convex TheoriesIFor each pair of shared variables x , y, determine if:1. F1 ⇒ x = y2. F2 ⇒ x = yIIf (1) holds but not (2), conjoin x = y with F2IIf (2) holds but not (1), conjoin x = y with F1ILet F10 and F20 denote new formulasICheck satisfiability of F10 and F20IRepeat until either formula becomes unsat or no new equalities can beinferredVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories23/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIFirst, we need to purify:Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIFirst, we need to purify:IReplace f (x ) with new variable w1Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIFirst, we need to purify:IReplace f (x ) with new variable w1IReplace f (y) with new variable w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIFirst, we need to purify:IReplace f (x ) with new variable w1IReplace f (y) with new variable w2If (x ) − f (y) is now replaced with w1 − w2 and we conjoinw1 = f (x ) ∧ w2 = f (y)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIFirst, we need to purify:IReplace f (x ) with new variable w1IReplace f (y) with new variable w2If (x ) − f (y) is now replaced with w1 − w2 and we conjoinw1 = f (x ) ∧ w2 = f (y)IFirst literal is now f (w1 − w2 ) 6= f (z ); still not pure!Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44ExampleIUse Nelson-Oppen to decide sat of following T= ∪ TQ formula:f (f (x ) − f (y)) 6= f (z ) ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIFirst, we need to purify:IReplace f (x ) with new variable w1IReplace f (y) with new variable w2If (x ) − f (y) is now replaced with w1 − w2 and we conjoinw1 = f (x ) ∧ w2 = f (y)IFirst literal is now f (w1 − w2 ) 6= f (z ); still not pure!IReplace w1 − w2 with w3 and add equality w3 = w1 − w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories24/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :Iw1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zWhich variables are shared?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :Iw1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zWhich variables are shared? allVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories25/44Example, contIPurified formula is F1 ∧ F2 where:F1 :F2 :w1 = f (x ) ∧ w2 = f (y) ∧ f (w3 ) 6= f (z )w3 = w1 − w2 ∧ x ≤ y ∧ y + z ≤ x ∧ 0 ≤ zIWhich variables are shared? allICheck sat of F1 .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
