6 Combination of decision procedures (1185842), страница 7
Текст из файла (страница 7)
Which disjunctions do we query?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44Nelson-Oppen with Non-Convex TheoriesIProblem is that in non-convex theories, a formula might imply adisjunction of equalitiesIBut it doesn’t have to imply any single equality on its ownIThus, it is not enough to query individual equality relations betweenvariablesIWe also have to query and propagate disjunctions of equalitiesITwo questions:1. Which disjunctions do we query?2. How do we propagate disjunctions since we are considering disjunction-freeformulas?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories32/44What Disjunctions to Query?IRecall: We only have a finite set of shared variablesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories33/44What Disjunctions to Query?IRecall: We only have a finite set of shared variablesIFrom these, we can only generate a finite number of disjunctions ofequalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories33/44What Disjunctions to Query?IRecall: We only have a finite set of shared variablesIFrom these, we can only generate a finite number of disjunctions ofequalitiesIThus, for each possible disjunction, we need to issue a queryVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories33/44What Disjunctions to Query?IRecall: We only have a finite set of shared variablesIFrom these, we can only generate a finite number of disjunctions ofequalitiesIThus, for each possible disjunction, we need to issue a queryIExample: If we have shared variables x , y, z , which queries do we need toissue?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories33/44What Disjunctions to Query?IRecall: We only have a finite set of shared variablesIFrom these, we can only generate a finite number of disjunctions ofequalitiesIThus, for each possible disjunction, we need to issue a queryIExample: If we have shared variables x , y, z , which queries do we need toissue?x =yx =zy =zx =y ∨x =zVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories33/44Propagating DisjunctionsISuppose answer to some disjunctive queryVijay Ganesh(Original notes from Isil Dillig),Wni=1ECE750T-28: Computer-aided Reasoning for Software Engineeringxi = yi is yesLecture 16: Decision Procedures for Combination Theories34/44Propagating DisjunctionsWnISuppose answer to some disjunctive queryIIn this case, we need to branch and consider all n possibilitiesVijay Ganesh(Original notes from Isil Dillig),i=1ECE750T-28: Computer-aided Reasoning for Software Engineeringxi = yi is yesLecture 16: Decision Procedures for Combination Theories34/44Propagating DisjunctionsWnISuppose answer to some disjunctive queryIIn this case, we need to branch and consider all n possibilitiesIThus, create n subproblems where we propagate xi = yi in i’thsubproblemVijay Ganesh(Original notes from Isil Dillig),i=1ECE750T-28: Computer-aided Reasoning for Software Engineeringxi = yi is yesLecture 16: Decision Procedures for Combination Theories34/44Propagating DisjunctionsWnISuppose answer to some disjunctive queryIIn this case, we need to branch and consider all n possibilitiesIThus, create n subproblems where we propagate xi = yi in i’thsubproblemIIf there is any subproblem that is satisfiable, original formula is satisfiableVijay Ganesh(Original notes from Isil Dillig),i=1ECE750T-28: Computer-aided Reasoning for Software Engineeringxi = yi is yesLecture 16: Decision Procedures for Combination Theories34/44Propagating DisjunctionsWnISuppose answer to some disjunctive queryIIn this case, we need to branch and consider all n possibilitiesIThus, create n subproblems where we propagate xi = yi in i’thsubproblemIIf there is any subproblem that is satisfiable, original formula is satisfiableIIf every subproblem is unsatisfiable, then original formula is unsatisfiableVijay Ganesh(Original notes from Isil Dillig),i=1ECE750T-28: Computer-aided Reasoning for Software Engineeringxi = yi is yesLecture 16: Decision Procedures for Combination Theories34/44ExampleIConsider T= ∪ TZ formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories35/44ExampleIConsider T= ∪ TZ formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IAfter purification, we get:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories35/44ExampleIConsider T= ∪ TZ formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IAfter purification, we get:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Which queries do we need to issue?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories35/44ExampleIConsider T= ∪ TZ formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IAfter purification, we get:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Which queries do we need to issue?(1) x = w1(2) x = w2(3) x = w1 ∨ x = w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories35/44ExampleIConsider T= ∪ TZ formula:1 ≤ x ∧ x ≤ 2 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (2)IAfter purification, we get:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 )1 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Which queries do we need to issue?(1) x = w1(2) x = w2(3) x = w1 ∨ x = w2IAnswer to queries (1) and (2) are no, but F2 implies query (3)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories35/44Example, contINow, we create two subproblems, one where we propagate x = w1 andx = w2Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories36/44Example, contINow, we create two subproblems, one where we propagate x = w1 andx = w2IFirst subproblem:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories36/44Example, contINow, we create two subproblems, one where we propagate x = w1 andx = w2IFirst subproblem:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Is this satisfiable?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories36/44Example, contINow, we create two subproblems, one where we propagate x = w1 andx = w2IFirst subproblem:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs this satisfiable?INo because x = w1 implies f (x ) = f (w1 )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories36/44Example, contISecond subproblem:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories37/44Example, contISecond subproblem:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2Is this satisfiable?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories37/44Example, contISecond subproblem:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs this satisfiable?INo because x = w2 implies f (x ) = f (w2 )Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories37/44Example, contISecond subproblem:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 2 ∧ w1 = 1 ∧ w2 = 2IIs this satisfiable?INo because x = w2 implies f (x ) = f (w2 )ISince neither subproblem is satisfiable, Nelson-Oppen returns unsat fororiginal formulaVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories37/44Example IIIConsider the following T= ∪ TZ formula:1 ≤ x ∧ x ≤ 3 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (3) ∧ f (1) 6= f (2)Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories38/44Example IIIConsider the following T= ∪ TZ formula:1 ≤ x ∧ x ≤ 3 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (3) ∧ f (1) 6= f (2)IFormulas after purification:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 )1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories38/44Example IIIConsider the following T= ∪ TZ formula:1 ≤ x ∧ x ≤ 3 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (3) ∧ f (1) 6= f (2)IFormulas after purification:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 )1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3Consider the query x = w1 ∨ x = w2 ∨ x = w3Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories38/44Example IIIConsider the following T= ∪ TZ formula:1 ≤ x ∧ x ≤ 3 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (3) ∧ f (1) 6= f (2)IFormulas after purification:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 )1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3IConsider the query x = w1 ∨ x = w2 ∨ x = w3IDoes either formula imply this query?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories38/44Example IIIConsider the following T= ∪ TZ formula:1 ≤ x ∧ x ≤ 3 ∧ f (x ) 6= f (1) ∧ f (x ) 6= f (3) ∧ f (1) 6= f (2)IFormulas after purification:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 )1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3IConsider the query x = w1 ∨ x = w2 ∨ x = w3IDoes either formula imply this query? YesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories38/44Example II, contIFirst subproblem:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories39/44Example II, contIFirst subproblem:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3Is this satisfiable?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories39/44Example II, contIFirst subproblem:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3Is this satisfiable? noVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories39/44Example II, contIFirst subproblem:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3IIs this satisfiable? noISecond subproblem:F1 :F2 :Vijay Ganesh(Original notes from Isil Dillig),f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories39/44Example II, contIFirst subproblem:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3IIs this satisfiable? noISecond subproblem:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3Is this satisfiable?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories39/44Example II, contIFirst subproblem:F1 :F2 :f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w11 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3IIs this satisfiable? noISecond subproblem:F1 :F2 :If (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w21 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3Is this satisfiable? YesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories39/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcIAre there any new implied equalities or disjunctions of equalities?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcIAre there any new implied equalities or disjunctions of equalities? NoVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcIAre there any new implied equalities or disjunctions of equalities? NoIThus, second subproblem is satisfiableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcIAre there any new implied equalities or disjunctions of equalities? NoIThus, second subproblem is satisfiableIDo we need to check third subproblem?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcIAre there any new implied equalities or disjunctions of equalities? NoIThus, second subproblem is satisfiableIDo we need to check third subproblem? NoVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44Example II, contSecond subproblem:IF1 : f (x ) 6= f (w1 ) ∧ f (x ) 6= f (w3 ) ∧ f (w1 ) 6= f (w2 ) ∧ x = w2F2 : 1 ≤ x ∧ x ≤ 3 ∧ w1 = 1 ∧ w2 = 2 ∧ w3 = 3So it’s satisfiable, are we done? No, need to check for new equalitiesIThus, we now issue new queries such as x = w1 , x = w2 , etcIAre there any new implied equalities or disjunctions of equalities? NoIThus, second subproblem is satisfiableIDo we need to check third subproblem? NoIThus, original formula is satisfiableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories40/44OptimizationIIn presentation so far, we issued some disjuctive queriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories41/44OptimizationIIn presentation so far, we issued some disjuctive queriesIAs soon as answer was yes to some query, we propagated it by performingcase splitVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories41/44OptimizationIIn presentation so far, we issued some disjuctive queriesIAs soon as answer was yes to some query, we propagated it by performingcase splitIBut really, we want to find a minimal query that is implied.Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories41/44OptimizationIIn presentation so far, we issued some disjuctive queriesIAs soon as answer was yes to some query, we propagated it by performingcase splitIBut really, we want to find a minimal query that is implied.IMinimal query is one where dropping any disjunct causes query to nolonger be impliedVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories41/44OptimizationIIn presentation so far, we issued some disjuctive queriesIAs soon as answer was yes to some query, we propagated it by performingcase splitIBut really, we want to find a minimal query that is implied.IMinimal query is one where dropping any disjunct causes query to nolonger be impliedIWhy do we want minimal query?Vijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories41/44OptimizationIIn presentation so far, we issued some disjuctive queriesIAs soon as answer was yes to some query, we propagated it by performingcase splitIBut really, we want to find a minimal query that is implied.IMinimal query is one where dropping any disjunct causes query to nolonger be impliedIWhy do we want minimal query?1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
