6 Combination of decision procedures (Презентации лекций), страница 8

Since x = y ∨ y = z already implies x = y ∨ y = z ∨ z = w , no need toconsider latter to decide satisfiabilityVijay 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. Since x = y ∨ y = z already implies x = y ∨ y = z ∨ z = w , no need toconsider latter to decide satisfiability2. When we propagate the query, using minimal query creates fewersubproblemsVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories41/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesIIf this isn’t implied, no subset will be implied, so we are doneVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesIIf this isn’t implied, no subset will be implied, so we are doneIIf it is implied, drop one equalityVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesIIf this isn’t implied, no subset will be implied, so we are doneIIf it is implied, drop one equalityIIf it is still implied, continue with smaller disjunctionVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesIIf this isn’t implied, no subset will be implied, so we are doneIIf it is implied, drop one equalityIIf it is still implied, continue with smaller disjunctionIOtherwise, restore equality and continue with next oneVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesIIf this isn’t implied, no subset will be implied, so we are doneIIf it is implied, drop one equalityIIf it is still implied, continue with smaller disjunctionIOtherwise, restore equality and continue with next oneIThis ensures we find a minimal disjunction that is impliedVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Optimization, cont.ITo find minimal query, start with disjunction of all possible equalitiesIIf this isn’t implied, no subset will be implied, so we are doneIIf it is implied, drop one equalityIIf it is still implied, continue with smaller disjunctionIOtherwise, restore equality and continue with next oneIThis ensures we find a minimal disjunction that is impliedIThist strategy much better than using any disjunction that is impliedVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories42/44Nelson-Oppen for Convex vs.

Non-Convex TheoriesINelson-Oppen method is much more efficient for convex theories than fornon-convex theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories43/44Nelson-Oppen for Convex vs. Non-Convex TheoriesINelson-Oppen method is much more efficient for convex theories than fornon-convex theoriesIIn convex theories:1. need to issue one query for each pair of shared variablesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories43/44Nelson-Oppen for Convex vs. Non-Convex TheoriesINelson-Oppen method is much more efficient for convex theories than fornon-convex theoriesIIn convex theories:1.

need to issue one query for each pair of shared variables2. If decision procedures for T1 and T2 have polynomial time complexity,combination using Nelson-Oppen also has polynomial complexityVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories43/44Nelson-Oppen for Convex vs. Non-Convex TheoriesINelson-Oppen method is much more efficient for convex theories than fornon-convex theoriesIIn convex theories:1. need to issue one query for each pair of shared variables2.

If decision procedures for T1 and T2 have polynomial time complexity,combination using Nelson-Oppen also has polynomial complexityIIn non-convex theories:1. need to consider disjunctions of equalities between each pair of sharedvariablesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories43/44Nelson-Oppen for Convex vs. Non-Convex TheoriesINelson-Oppen method is much more efficient for convex theories than fornon-convex theoriesIIn convex theories:1. need to issue one query for each pair of shared variables2. If decision procedures for T1 and T2 have polynomial time complexity,combination using Nelson-Oppen also has polynomial complexityIIn non-convex theories:1.

need to consider disjunctions of equalities between each pair of sharedvariables2. If decision procedures for T1 and T2 have NP time complexity,combination using Nelson-Oppen also has NP time complexityVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories43/44SummaryINelson-Oppen method gives a sound and complete decision procedure forcombination theoriesVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories44/44SummaryINelson-Oppen method gives a sound and complete decision procedure forcombination theoriesIHowever, it only works for quantifier-free theories that are infinitely stableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories44/44SummaryINelson-Oppen method gives a sound and complete decision procedure forcombination theoriesIHowever, it only works for quantifier-free theories that are infinitely stableINot a severe restriction because most theories of interest are infinitelystableVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories44/44SummaryINelson-Oppen method gives a sound and complete decision procedure forcombination theoriesIHowever, it only works for quantifier-free theories that are infinitely stableINot a severe restriction because most theories of interest are infinitelystableINext lecture: How to decide satisfiability in first-order theories withoutconverting to DNFVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories44/44SummaryINelson-Oppen method gives a sound and complete decision procedure forcombination theoriesIHowever, it only works for quantifier-free theories that are infinitely stableINot a severe restriction because most theories of interest are infinitelystableINext lecture: How to decide satisfiability in first-order theories withoutconverting to DNFIReminder: homework due next lectureVijay Ganesh(Original notes from Isil Dillig),ECE750T-28: Computer-aided Reasoning for Software EngineeringLecture 16: Decision Procedures for Combination Theories44/44.