歡迎來到裝配圖網(wǎng)! | 幫助中心 裝配圖網(wǎng)zhuangpeitu.com!
裝配圖網(wǎng)
ImageVerifierCode 換一換
首頁 裝配圖網(wǎng) > 資源分類 > PPT文檔下載  

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

  • 資源ID:241838437       資源大?。?span id="6tqzmsl" class="font-tahoma">541.50KB        全文頁數(shù):63頁
  • 資源格式: PPT        下載積分:16積分
快捷下載 游客一鍵下載
會員登錄下載
微信登錄下載
三方登錄下載: 微信開放平臺登錄 支付寶登錄   QQ登錄   微博登錄  
二維碼
微信掃一掃登錄
下載資源需要16積分
郵箱/手機:
溫馨提示:
用戶名和密碼都是您填寫的郵箱或者手機號,方便查詢和重復下載(系統(tǒng)自動生成)
支付方式: 支付寶    微信支付   
驗證碼:   換一換

 
賬號:
密碼:
驗證碼:   換一換
  忘記密碼?
    
友情提示
2、PDF文件下載后,可能會被瀏覽器默認打開,此種情況可以點擊瀏覽器菜單,保存網(wǎng)頁到桌面,就可以正常下載了。
3、本站不支持迅雷下載,請使用電腦自帶的IE瀏覽器,或者360瀏覽器、谷歌瀏覽器下載即可。
4、本站資源下載后的文檔和圖紙-無水印,預覽文檔經(jīng)過壓縮,下載后原文更清晰。
5、試題試卷類文檔,如果標題沒有明確說明有答案則都視為沒有答案,請知曉。

數(shù)學邏輯分析-無原因推理 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

注意事項

本文(數(shù)學邏輯分析-無原因推理 Non-clausal Reasoning)為本站會員(ra****d)主動上傳,裝配圖網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護處理,對上載內(nèi)容本身不做任何修改或編輯。 若此文所含內(nèi)容侵犯了您的版權或隱私,請立即通知裝配圖網(wǎng)(點擊聯(lián)系客服),我們立即給予刪除!

溫馨提示:如果因為網(wǎng)速或其他原因下載失敗請重新下載,重復下載不扣分。




關于我們 - 網(wǎng)站聲明 - 網(wǎng)站地圖 - 資源地圖 - 友情鏈接 - 網(wǎng)站客服 - 聯(lián)系我們

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

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


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