数学逻辑分析-无原因推理 Non-clausal Reasoning

Non-clausal ReasoningFahiem Bacchus,Christian Thiffault,TorontoToby Walsh,UCC&Uppsala(soon UNSW,NICTA,Uppsala)Every morning I read the plaque on the wall of this house Dedicated to the memory of George Boole Professor of Mathematics at Queens College(now University College Cork)George Boole(1815-1864)nBoolean algebraThe Mathematical Analysis of Logic,Cambridge,1847The Calculus of Logic,Cambridge and Dublin Mathematical journal,1848nReduce propositional logic to algebraic manipulationsGeorge Boole(1815-1864)nBoolean algebraThe Mathematical Analysis of Logic,Cambridge,1847The Calculus of Logic,Cambridge and Dublin Mathematical journal,1848nReduce propositional logic to algebraic manipulationsHow do we automate reasoning with propositional formulae?Propositional SATisfiabilitynRapid progress being maden10 years ago,1000 varsnAlgorithmic advancesnLearningnWatched literalsn.nHeuristic advancesnVSIDS branching Propositional SATisfiabilitynEfficient implementationsnChaff,Berkmin,Forklift,nSAT competition has new winner almost every yearnPractical applicationsnHardware verificationnPlanningnSAT folklorenNeed to solve in CNFnEverything is a clausenEfficient reasoningnOptimize code with simple data structures nEffective reasoningnConversion into CNF does not hinder unit propagationOverturning SAT folklorenDeciding arbitrary Boolean formulaenWithout converting into CNFnEfficient reasoningnRaw speed as good as optimized CNF solversnEffective reasoningnMore inference than unit propagationnExploit structurenMore exotic gates,Davis Putnam procedureDPLL(S)if S empty then SATif S contains then UNSATif S contains unit,l then DPLL(S u l)else chose literal,l if DPLL(S u l)then SAT else DPLL(S u-l)Unit PropagationnIf the formula has a unit clause then the literal in that clause must be truenSet the literal to true and reduce the formula.nUnit propagation is the most commonly used type of constraint propagationnOne of the most important parts of current SAT solvers Unit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)Unit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)a=trueUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)a=trueUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)a=trueUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)a=trueUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)b=falseUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)b=falseUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)b=falseUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)c=trueUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)c=trueUnit Propagation(a)(-a,b,c)(-b)(a,d,e)(-c,d,g)c=trueImplementing Unit PropagationnUP is main(often only)inference rule applied at each search node.nPerforming UP occupies most of the time in these solvers.nMore efficient implementations of UP has been one of the recent advances.Implementing Unit PropagationnMost DPLL solvers do not build an explicit representation of the reduced formulanToo expensive in time and space to do this.nRather they keep original formula and mark the changes madenAll changes generated by UP undone when we backtrack.Tableau Crawford and Auton 95nWe number the variables and clauses.nEach variable hasna field to store its current value,true,false or unvaluednthe list of clauses it appears positively innthe list of clauses it appears negatively innEach clause hasna list of its literalsna flag to indicate whether or not it is satisfiednthe number of unvalued literals it containsTableau Crawford and Auton 95nUnit propagated literal put on a stacknpop the literal on top of the stacknmark the variable with the appropriate value.nmark each clause it appears positively in as satisfied.nfor each clause it appears negatively innif the clause is not already satisfied decrement the clauses counternif the counter is equal to 1,the clause is unitnfind the single unvalued literal in the clause and add that literal to the UP stack.nremember all changes so that they can be undone on backtrack.Watch literals SATO,ChaffnTableaus technique requires visiting each clause a variable appears in when we value a variable.nWhen clause learning is employed,and 100,000s of long new clauses are added to the original formula this becomes slow.nThe watch literal technique is more efficient.Watch literals SATO,ChaffnFor each clause,pick two literals to watch.nAt least one of these literals must be false for the clause to be unit.nFor each variable instead of lists of all of the clauses it appears in positively and negatively,we only have lists of the clauses it is a watch for.nreduces the total size of these lists from O(kn)to O(n)Watch literals SATO,ChaffnWhen we assign a value to a variable wenIgnore the clauses it watches positivelynFor each clause it watches negatively,we search the clause:nif we find an unvalued literal or a true literal not equal to the other watch we replace this literal the watchnotherwise the clause is unit and we UP the other watch literal if it is not already true.nOn backtrack we do nothing!nThe new watch literals retain the property that at least one of them must become false if the clause is to become unit.Solving non-CNF formulaenConvert into CNFnUse efficient DPLL solver like ChaffnAdapt DPLL solver to reason with non-CNFnExploit structurenPermit complex gates(eg counting,XOR,.)Encoding into CNFnMost common(and relatively efficient?)is that of Tseitin 1970.nRecusively converts a formula by adding a new variable for every subformula.nLinear spaceTseitin EncodingA (C&D)1.(V1,C)2.(V1,D)3.(C,D,V1)Tseitin EncodingA (C&D)V1 (C&D)(V1,C),(V1,D),(C,D,V1)1.(V1,C)2.(V1,D)3.(C,D,V1)4.(V2,A,V1)5.(A,V2)6.6.(V1,V2)Tseitin EncodingA (C&D)V1 (C&D)(V1,C),(V1,D),(C,D,V1)V2 (A V1)(V2,A,V1),(A,V2),(V1,V2)1.(V1,C)2.(V1,D)3.(C,D,V1)4.(V2,A,V1)5.(A,V2)6.(V1,V2)7.7.(V2)Tseitin EncodingA (C&D)V1 (C&D)(V1,C),(V1,D),(C,D,V1)V2 (A V1)(V2,A,V1),(A,V2),(V1,V2)Disadvantage of CNF nStructural information is lostnFlattens formulae into clauses.nIn a Boolean circuitnWhich variables are inputs?nWhich are internal wires?n nAdditional variables are added.nPotentially increases the size of the DPLL search.Structural Information nNot all structural information can be recovered Lang&Marquis,1989.nRecovering structural information can improve performance EqSatZ,LSAT.nWhy lose this information in the first place?nIn addition,we can exploit more complex gatesExtra VariablesnPotentially“increase search spacenDo not branch on any on the newly introduced“subformula variables.nTheoretically this can increase exponentially the size of smallest DPLL proof Jarvisalo et al.2004nEmpirically solvers restricted in this way can perform poorlyExtra VariablesnThe alternative is unrestricted branching.nHowever,with unrestricted branching,a CNF solver can waste a lot of time branching on variables that have become“irrelevant.Irrelevant Variables A (C&D)A=false formula satisfied1.(V1,C)2.(V1,D)3.(C,D,V1)4.(V2,A,V1)5.(A,V2)6.(V1,V2)7.(V2)8.(A)Solver must still determine that the remaining clauses are SATIrrelevant VariablesA (C&D)V1 (C&D)V2 (A V1)Converting to CNF is Unnecessary nSearch can be performed on the original formula.nThis has been noted in previous work on circuit based solvers,e.g.Ganai et al.2002nReasoning with the original formula may permit other efficienciesnE.g.exploiting structure,&complex gatesDPLL on formulae nView formulae as DAGsnEvery node has a label(True/False/Unassigned)nBranch on the truth value of any unassigned nodenUse Boolean logic to propagate truth values to neighbouring nodesnContradiction when node is labeled both True and FalsenFind consistent labeling with truth values that assigns True to root(SAT)nOr exhaust all possibilities(UNSAT)/xorA B&C D TrueFalse/&C D Labeling unit propagation nLabeling a node assigning a truth value to corresponding var in CNF encodingnPropagating labels in the DAG unit propagation in the CNF encoding Learning nOnce a contradiction is detected a conflict clause can be learnednset of impossible node assignmentsncan use 1-UIP scheme(as in CNF solvers)nLearned clauses stored and used to unit propagate node truth values Complex gates nGates can have arbitrary degreenn-ary AND,n-ary OR,nGates can be complicated Boolean functionsnn-ary XOR(which requires exponential number of CNF clauses)ncardinality gates(at least one,k out of n,.)Label propagation nUse lazy data structures as in CNF solversnFor example.assign one child as a true watch for an AND gatenDont check if AND gate can be labeled true until its true watch becomes true nSome benchmarks have AND gates with thousands of childrennNo intrinsic loss of efficiency in using the DAG over CNF.Structure based optimizationsnWe can also exploit the extra structural information the DAG providesnTwo such optimizationsnDont care propagation to deal with irrelevant subformulaenConflict clause reductionDont Care labelingnAdd a third“truth value to the DAG:“dont carenA node C is dont care wrt a particular parent P nIf its truth value can no longer affect the truth value of P nor any of its P siblings.nOr P is dont care.nA node C is dont care if it is dont care wrt to all of its parentsnNo need to branch on dont cares!Dont Care labelingnAssign a dont care watch parent for each node.nWhen P is labeled,C can becom dont care wrt to its watch parent PnIf C becomes dont care wrt to its dont care watch we look for another watch.nIf we cant find one we know,C has become dont care/xorB&C D TrueFalse/&C D Dont careA A xorB Conflict Clause ReductionsnIf one learns(L1,L2,.)and one has(L1,L2)then we can reduce the conflict clausen(L1,L2)resolves with(L1,L2,.)to give(L2,.)nResult subsumes the original conflict clausenIn CNF,we would have to search the clause database to detect this situationnProbably not going to be effectiveConflict Clause ReductionsnSuppose P is an AND node,and C is a childnThen C implies PnIf we have the conflict clause:n(P,C,X,)nThis reduces ton(P,X,)nEquivalent to a resolution step against(C,P)Conflict Clause ReductionsnWhen conflict clause generatednSearch neighbours in DAG for such reductionsnMore useful on“shorter clausesnExperimentally found it only worth looking for such reductions on clauses of length 100 or lessEmpirical Results.nWe compared with ZchaffnTried to isolate impact of CNF v non-CNFnMade the two solvers as close as possiblenSame magic numbers(e.g.,clause database cleanup criteria,restart intervals etc.)nSame branching heuristicsnExpect similar improvements could be obtained with others CNF solversEmpirical Results caveats nLack of non-clausal benchmarksnHope SAT-05 competition will include non-CNFnBenchmarks we did obtain had already been transformed into simpler formulasnNo complex XOR or IFF gatesFVP-UNSAT-2.0(Velev)Time FVP-UNSAT-2.0 Decisions FVP-UNSAT-2.0 Dont CaresFVP-UNSAT-2.0 Clause ReductionOther SeriesConclusionsnNo intrinsic reason to convert to CNFnMany other structure based optimizations remain to be investigatednBranching heuristicsnNon-clausal conflictsnMore complex gatesn