DecidingseparationformulaswithSAT

Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,Click to edit Master title style,Deciding separation formulas with SAT,Ofer Strichman Sanjit A. Seshia Randal E. Bryant,School of Computer Science,Carnegie Mellon University,1,Separation predicates,Predicates of the form,x,1,x,2,+,c,and,x,1,x,2,+,c,where,c,is a constant,Also known as difference predicates,We will consider,x,1,x,2,as either real or integer variables,Used when proving formulas derived from,Timed automata,Scheduling problems, and more,Pratt: “Most inequalities arising in verification are separation predicates”,2,Deciding separation via case-splitting (,1,/2),:,x,1,x,2,+ 1,x,2,x,3,+ 1,(,x,3,x,1,-3,x,3,x,1,+1,),x,1,x,2,+ 1,x,2,x,3,+ 1,x,3,x,1,-3,x,1,x,2,+ 1,x,2,x,3,+ 1,x,3,x,1,+1,x,1,x,2,x,3,1,1,-3,x,1,x,2,x,3,1,1,1,Theorem Bellman, 57,: The formula is satisfiable,iff,t,he,inequality graph does not contain a negative cycle.,Case splitting,3,Deciding separation via case-splitting (2/2),1,1,-3,5,-4,Bellman-Ford:,Finding whether there is a negative,cycle in a graph is polynomial,Overall complexity: O(2,|,|,), due to case-splitting,Case,-,splitting is normally the bottleneck of decision procedures,Q: Is there an alternative to case-splitting ?,4,Difference Decision Diagrams(DDD),(M,ller, Lichtenberg, Andersen, Hulgaard, 1999),Similar to BDDs, but the nodes are separation predicates,Ordering on variables determines order on predicates,Semi-canonical (i.e canonical when,is a tautology or a contradiction),:,!(,x,1, x,3, 0,),x,2,-,x,3,0,!(,x,2,-x,1,0,),x,1, x,3, 0,x,2,-,x,3,0,x,2,-x,1,0,1,0,Each path leading to 1 is checked for consistency with Bellman-Ford,Worst case an exponential no. of such paths,5,:,x,1,x,2,+ 1 ,x,2,x,3,+ 1 (,x,3,x,1,-3 ,x,3,x,1,+1),1.,Encode:,2.,Build the joint graph,G,:,x,1,x,2,x,3,1,1,1,-3,3.,Forbid true,assignment to negative simple cycles in,G,:,Boolean encoding (take 1),:,6,What about negations in,?,The,unsatisfiable,formula,:,(,x,1, x,2,x,2,x,1,+,1),i,s reduced to the,satisfiable,formula:,x,1,x,2,0,1,Problem: our graph does not consider the polarity of the constraints.,Legend,:,7,Solution #1: Consider both polarities,Dual edges:,x,1,x,2,x,3,1,1,-3,x,1,x,2,x,3,-1,-1,3,x,1,x,2,x,3,1,1,-3,-1,-1,3,The joint graph:,x,1, and , predicates as ,x,2,+ c,as,x,2,x,1, c,Solution #2 results in a smaller number of constraints,9,Problem: redundant constraints,:,(,x,1,x,2,-3,(,x,2,x,3,1,x,3,x,1,+1,),x,1,x,3,x,2,-3,-1,x,1,x,3,x,2,-3,1,Case splitting,x,1,x,3,x,2,-3,1,-1,The joint graph,G,:,G,creates redundant constraints,10,Let,d,be the DNF representation of,Solution: Conjunctions Matrices (1/3),We only need to consider cycles that are in one of the clauses of,d,Deriving,d,is exponential. But ,Knowing whether a given set of literals share a clause in,d,is polynomial, using,Conjunctions Matrices,11,Conjunctions Matrices (2/3),Let,be a formula in NNF.,Let,l,i,and,l,j,be two literals in,.,The,joining operand,of,l,i,and,l,j,is the lowest joint parent of,l,i,and,l,j,in the parse tree of,.,:l,0,(,l,1,(,l,2,l,3,),l,0,l,1,l,2,l,3,l,0,l,1,l,2,l,3,l,0,l,1,l,2,l,3,1 1 1,1 0 0,1 0 1,1 0 1,Conjunctions Matrix,M,:,12,Claim: A set of literals,L=,l,0,l,1,l,n, ,share a clause in,d,iff for all,l,i,l,j,L,i,j,M,l,i,l,j, =1,.,:,x,0,x,1,(,x,1,x,2,(,x,2,x,3,x,3,x,0,),x,0,x,3,x,2,x,1,Conjunctions Matrices (3/3),In our case the literals are separation predicates.,The entries in the conjunctions matrix correspond to edges between edges,We can now consider only simple cycles that their corresponding,M,graph form a clique,.,13,1.,Encode,(replace each separation predicate with a Boolean var),2.,Build the joint inequality graph,G,3.,Add a constraint forbidding true assignment to,negative simple cycles in,G,that their corresponding,M,form a clique.,0.,Normalize,(eliminate,negations),Boolean encoding (take 2),14,.,In many cases - yes.,How? with variable elimination,.,c,1,c,2,c,1+,c,2,n,diamonds,2,n,simple cycles.,Can we do better than that ?,c,3,c,4,Compact representation of constraints (1/2),15,Quantifying out,x,3,:,Worst case exponential no. of constraints,Complexity heavily depends on elimination order,c,1,c,2,c,3,c,1,+ c,3,c,2,+ c,3,x,4,x,1,x,1,x,2,x,3,x,4,x,4,x,2,Compact representation of constraints (2/2),Given a conjunctions matrix,M, we add a constraint only if the joining operand of the two constraints is ,16,1.,Encode,(replace each separation predicate with a Boolean var),2.,Build the joint inequality graph,G,3.,Eliminate all variables successively:,e,1,and,e,2,are ingoing and outgoing edges of the eliminated variable,and,M,e,1,e,2,=1,and,the resulting edge is,e,3,then,add,to,the constraint,e,1,e,2,e,3,0.,Normalize,(eliminate,negations),Boolean encoding (take 3),If,17,Extension to integer variables,Given,with,integer,separation predicates, derive,R,:,Declare all variables as,real,Replace,x,1,x,2,+ c,and,x,1,x,2,+ c,where,c,is not an integer,with,x,1,x,2,+,c,Replace each predicate,x,1,y,+,c,where,x,y,are real variables, and,c,is a constant,Pratt 73 (/Bellman57):,Given a set of conjuncted separation predicates,1. Construct the inequality graph,2.,is satisfiable iff there is no cycle with non-negative accumulated weight,:,(,x,z,+3,z,y,1,y,x,+1,),x,y,z,3,1,-1,26,Handling,d,isjunctions through case splitting,All previously mentioned algorithms handle disjunctions,by splitting the formula.,This can be thought of as a two stage process:,Convert formula to Disjunctive Normal Form (DNF),Solve each clause separately, until satisfying one of them.,(A common improvement: split when needed),Case splitting is frequently the bottleneck of the procedure,27,So what can be done against case-splitting ?,Given a formula, t,his transformation can be done if,s.t. |,=,|,=, and,is decidable under a finite domain.,When is this possible?,enjoys the Small model property, or,Tailor-made reduction,Answer:,Split the domain, not the formula,.,28,SAT vs. infinite-state decision procedures,With finite instantiation (e.g. SAT), we split the,domain,.,Infinite state decision procedures split the,formula,.,So whats the big difference ?,29,SAT vs. infinite-state decision procedures,1.,Pruning.,2.,Learning.,3.,Guidance (prioritizing internal steps),Three mechanisms, crucial for efficient decision making:,SAT has a significant advantage in all three.,30,SAT vs. infinite-state decision procedures (1/4),1.,Pruning,SAT,: each clause,c,prunes,up to,2,|v|-|,c,|,states.,Others,: ? (stops when finds a satisfiable clause),y,x,0,0,1,1,Backtrack,Pruned!,.,(,x,y),.,.,|,v|=1000, |,c,| =2,Pruning,2,998,states,31,SAT vs. infinite-state decision procedures (2/4),2.,Learning,SAT,: Partial assignments that,lead,to a conflict are recorded and,hence not repeated.,Others,: (depends on decision procedure),- Adding proved sub-goals as antecedents to new sub-goals,- ,32,SAT vs. infinite-state decision procedures (3/4),3.,Guidance (prioritizing internal steps),Guidance requires efficient estimation:,Consider,1, ,2, where,1,is,unsat,and hard, and,2,is,sat,and easy.,With proper guidance, a theorem prover should start from,2,.,- How hard it is to solve each sub-formula?,- To what extent will it simplify the rest of the proof?,33,SAT vs. infinite-state decision procedures (4/4),3.,Guidance (contd),“.To what extent will it simplify the rest of the proof?”,SAT,: Guidance through decision heuristics (e.g. DLIS).,Others,: Expression ordering, .,(,x,y,z),(x,v),(x,z),Estimating simplification by counting literals,in each phase,34,This work,Separation predicates:,Separation predicates for integers:,Linear arithmetic:,Integer linear arithmetic:,Extends the results of Bryant et.al. to,a Boolean combination of,:,This,work,35,Reducing separation predicates to propositional logic (4/6),B. Encode predicates and construct a graph (procedure),Let, ,1.,Construct a graph,G,(,V,E,), where,V,= variables in,.,Each edge,e,E,is a 4-tuple,(,from,to,weight, ),2.,Substitute each predicate in,of the form,x y+c,with a,Boolean variable , and add an edge,(x,y,c, ),to,E,36,x,y,z,3,1,-1,Reducing separation predicates to propositional logic (3/6),:,(,x,z,+3,(,z,y,1,y,x,+1,),:,Transitivity,constraints,(,),(,B. Encode + construct graph (example):,Separation graph:,37,If total weight is positive,or,All edges are , and total weight is equal to 0,then add the constraint:,C. Add transitivity constraints for each cycle,C,Reducing separation predicates to propositional logic (6/6),38,x,y,z,3,1,-1,Reducing separation predicates to propositional logic (5/6),:,Transitivity,constraints,(,),(,C. Add transitivity constraints for each simple cycle (example):,:,(,(,),(,),(,39,Some special cases:,1.,If the diamonds are balanced, O(,n,) constraints,.,c,1,c,1,c,1,c,1,c,2,c,2,c,2,c,2,2.,If there are uniform weights,c,1,and,c,2,c,1,c,2,on top and bottom,paths O(,n,2,) constraints,Compact representation of,c,onstraints,40,Integrated decision procedures in Theorem-Provers,Deciding a combination of theories is the key for automation,in Theorem Provers:,Boolean operators, Bit-vector, Sets,Linear-Arithmetic,Uninterpreted functions, More ,f(f(x)-f(y) != f(z) & y 10,Uninterpreted functions,Linear Arithmetic,Bit-Vector,operators,Normally, each theory is solved with,i,t,s,own decision procedure,And the results are combine,d (,Shostak,Nelson,.),.,41,