GRASP-an efficient SAT solverWhat is SAT?Slide 3Why SAT?OutlineTerminologySlide 7Basic Backtracking SearchSlide 9Backtracking Search in ActionSlide 11Davis-Putnam revisitedGRASPGRASP search templateGRASP Decision HeuristicsGRASP DeductionImplication GraphsExample Implication GraphGRASP Deduction ProcessGRASP Conflict AnalysisLearningSlide 22Learning (some math)Slide 24Slide 25BacktrackingContinued IGSlide 28Slide 29Procedure Diagnose()Is that all?GRASP-an efficient SAT solverPankaj Chauhan01/14/19 15-398: GRASP and Chaf 2What is SAT?Given a propositional formula in CNF, find an assignment to boolean variables that makes the formula true!E.g.1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)A = {x1=0, x2=1, x3=0, x4=1} 1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)A = {x1=0, x2=1, x3=0, x4=1} SATisfying assignment!01/14/19 15-398: GRASP and Chaf 3What is SAT?Solution 1: Search through all assignments!n variables  2n possible assignments, explosion!SAT is a classic NP-Complete problem, solve SAT and P=NP!01/14/19 15-398: GRASP and Chaf 4Why SAT?Fundamental problem from theoretical point of viewNumerous applicationsCAD, VLSIOptimizationModel Checking and other type of formal verificationAI, planning, automated deduction01/14/19 15-398: GRASP and Chaf 5OutlineTerminologyBasic Backtracking SearchGRASPPointers to future workPlease interrupt me if anything is not clear!01/14/19 15-398: GRASP and Chaf 6TerminologyCNF formula x1,…, xn: n variables1,…, m: m clausesAssignment ASet of (x,v(x)) pairs|A| < n  partial assignment {(x1,0), (x2,1), (x4,1)} |A| = n  complete assignment {(x1,0), (x2,1), (x3,0), (x4,1)} |A= 0  unsatisfying assignment {(x1,1), (x4,1)}|A= 1  satisfying assignment {(x1,0), (x2,1), (x4,1)}1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)A = {x1=0, x2=1, x3=0, x4=1} 1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)A = {x1=0, x2=1, x3=0, x4=1}01/14/19 15-398: GRASP and Chaf 7TerminologyAssignment A (contd.)|A= X  unresolved {(x1,0), (x2,0), (x4,1)}An assignment partitions the clause database into three classesSatisfied, unsatisfied, unresolvedFree literals: unassigned literals of a clauseUnit clause: #free literals = 101/14/19 15-398: GRASP and Chaf 8Basic Backtracking SearchOrganize the search in the form of a decision treeEach node is an assignment, called decision assignmentDepth of the node in the decision tree  decision level (x)x=v@d  x is assigned to v at decision level d01/14/19 15-398: GRASP and Chaf 9Basic Backtracking SearchIterate through:1. Make new decision assignments to explore new regions of search space2. Infer implied assignments by a deduction process. May lead to unsatisfied clauses, conflict! The assignment is called conflicting assignment.3. Conflicting assignments leads to backtrack to discard the search subspace01/14/19 15-398: GRASP and Chaf 10Backtracking Search in Action1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4) x1 x1 = 0@1{(x1,0), (x2,0), (x3,1)} x2 x2 = 0@2{(x1,1), (x2,0), (x3,1) , (x4,0)} x1 = 1@1 x3 = 1@2 x4 = 0@1 x2 = 0@1 x3 = 1@1No backtrack in this example!01/14/19 15-398: GRASP and Chaf 11Backtracking Search in Action1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)4 = (x1  x2  x3)1 = (x2  x3) 2 = (x1  x4)3 = (x2  x4)4 = (x1  x2  x3)Add a clause x4 = 0@1 x2 = 0@1 x3 = 1@1conflict{(x1,0), (x2,0), (x3,1)} x2 x2 = 0@2 x3 = 1@2 x1 = 0@1 x1 x1 = 1@101/14/19 15-398: GRASP and Chaf 12Davis-Putnam revisitedDeductionDecisionBacktrack01/14/19 15-398: GRASP and Chaf 13GRASPGRASP is Generalized seaRch Algorithm for the Satisfiability Problem (Silva, Sakallah, ’96)Features:Implication graphs for BCP and conflict analysisLearning of new clausesNon-chronological backtracking!01/14/19 15-398: GRASP and Chaf 14GRASP search template01/14/19 15-398: GRASP and Chaf 15GRASP Decision HeuristicsProcedure decide()Choose the variable that satisfies the most #clauses == max occurences as unit clauses at current decision levelOther possibilities exist01/14/19 15-398: GRASP and Chaf 16GRASP DeductionBoolean Constraint Propagation using implication graphsE.g. for the clause  = (x  y), if y=1, then we must have x=1For a variable x occuring in a clause , assignment 0 to all other literals is called antecedent assignment A(x)E.g. for  = (x  y  z), A(x) = {(y,0), (z,1)}, A(y) = {(x,0),(z,1)}, A(z) = {(x,0), (y,0)} Variables directly responsible for forcing the value of xAntecedent assignment of a decision variable is empty01/14/19 15-398: GRASP and Chaf 17Implication GraphsNodes are variable assignments x=v(x) (decision or implied)Predecessors of x are antecedent assignments A(x)No predecessors for decision assignments!Special conflict vertices have A() = assignments to vars in the unsatisfied clauseDecision level for an implied assignment is(x) = max{(y)|(y,v(y))A(x)}01/14/19 15-398: GRASP and Chaf 18Example Implication Graph1 = (x1  x2) 2 = (x1  x3  x9)3 = (x2  x3  x4)4 = (x4  x5  x10)5 = (x4  x6  x11)6 = (x5  x6)7 = (x1  x7  x12)8 = (x1 x8)9 = (x7  x8   x13)1 = (x1  x2) 2 = (x1  x3  x9)3 = (x2  x3  x4)4 = (x4  x5  x10)5 = (x4  x6  x11)6 = (x5  x6)7 = (x1  x7  x12)8 = (x1 x8)9 = (x7  x8   x13)Current truth assignment: {x9=0@1 ,x10=0@3, x11=0@3, x12=1@2, x13=1@2}Current decision assignment: {x1=1@6}66 conflictx9=0@1x1=1@6x10=0@3x11=0@3x5=1@64455x6=1@622x3=1@61x2=1@633x4=1@601/14/19 15-398: GRASP and Chaf 19GRASP Deduction Process01/14/19 15-398: GRASP and Chaf 20GRASP Conflict AnalysisAfter a conflict arises, analyze the implication graph at current decision levelAdd new clauses that would prevent the occurrence of the same conflict in the future  LearningDetermine decision level to backtrack to, might not be the immediate one  Non-chronological backtrack01/14/19 15-398: GRASP and Chaf 21LearningDetermine the assignment that