數(shù)學(xué)邏輯分析-無(wú)原因推理 Non-clausal Reasoning

上傳人:ra****d 文檔編號(hào):241838437 上傳時(shí)間:2024-07-29 格式:PPT 頁(yè)數(shù):63 大小:541.50KB
收藏 版權(quán)申訴 舉報(bào) 下載
數(shù)學(xué)邏輯分析-無(wú)原因推理 Non-clausal Reasoning_第1頁(yè)
第1頁(yè) / 共63頁(yè)
數(shù)學(xué)邏輯分析-無(wú)原因推理 Non-clausal Reasoning_第2頁(yè)
第2頁(yè) / 共63頁(yè)
數(shù)學(xué)邏輯分析-無(wú)原因推理 Non-clausal Reasoning_第3頁(yè)
第3頁(yè) / 共63頁(yè)

下載文檔到電腦,查找使用更方便

16 積分

下載資源

還剩頁(yè)未讀,繼續(xù)閱讀

資源描述:

《數(shù)學(xué)邏輯分析-無(wú)原因推理 Non-clausal Reasoning》由會(huì)員分享,可在線閱讀,更多相關(guān)《數(shù)學(xué)邏輯分析-無(wú)原因推理 Non-clausal Reasoning(63頁(yè)珍藏版)》請(qǐng)?jiān)谘b配圖網(wǎng)上搜索。

1、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-186

2、4)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,C

3、ambridge 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 advance

4、snVSIDS 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 simp

5、le 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 propagation

6、nExploit 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 true

7、nSet 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

8、,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 Prop

9、agation(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.

10、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

11、 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

12、 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

13、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 un

14、done 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 effi

15、cient.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.nre

16、duces 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

17、 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 formulaenConver

18、t 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 subformu

19、la.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.(

20、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.

21、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 g

22、atesExtra 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

23、 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

24、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

25、 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

26、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 propagatio

27、n 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-

28、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

29、 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

30、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

31、 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

32、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

33、,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)Co

34、nflict 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

35、 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 c

36、ompetition 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

展開(kāi)閱讀全文
溫馨提示:
1: 本站所有資源如無(wú)特殊說(shuō)明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請(qǐng)下載最新的WinRAR軟件解壓。
2: 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請(qǐng)聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
3.本站RAR壓縮包中若帶圖紙,網(wǎng)頁(yè)內(nèi)容里面會(huì)有圖紙預(yù)覽,若沒(méi)有圖紙預(yù)覽就沒(méi)有圖紙。
4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
5. 裝配圖網(wǎng)僅提供信息存儲(chǔ)空間,僅對(duì)用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對(duì)用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對(duì)任何下載內(nèi)容負(fù)責(zé)。
6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請(qǐng)與我們聯(lián)系,我們立即糾正。
7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對(duì)自己和他人造成任何形式的傷害或損失。

相關(guān)資源

更多
正為您匹配相似的精品文檔
關(guān)于我們 - 網(wǎng)站聲明 - 網(wǎng)站地圖 - 資源地圖 - 友情鏈接 - 網(wǎng)站客服 - 聯(lián)系我們

copyright@ 2023-2025  zhuangpeitu.com 裝配圖網(wǎng)版權(quán)所有   聯(lián)系電話:18123376007

備案號(hào):ICP2024067431號(hào)-1 川公網(wǎng)安備51140202000466號(hào)


本站為文檔C2C交易模式,即用戶上傳的文檔直接被用戶下載,本站只是中間服務(wù)平臺(tái),本站所有文檔下載所得的收益歸上傳人(含作者)所有。裝配圖網(wǎng)僅提供信息存儲(chǔ)空間,僅對(duì)用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對(duì)上載內(nèi)容本身不做任何修改或編輯。若文檔所含內(nèi)容侵犯了您的版權(quán)或隱私,請(qǐng)立即通知裝配圖網(wǎng),我們立即給予刪除!