對(duì)可滿足性(SAT)問題求全解的算法研究及實(shí)現(xiàn).pdf

1、北京交通大學(xué)碩士學(xué)位論文對(duì)可滿足性（SAT）問題求全解的算法研究及實(shí)現(xiàn)姓名：趙偉楠申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：計(jì)算機(jī)科學(xué)與技術(shù)指導(dǎo)教師：吳為民20090601ABSTRACTABSTRACT：AsthefirstprovedNPcompleteproblem，satisfiabilityproblem(SAT)hascmcmlsignificancebothintheoreticalresearchandpracticalapplicati

2、onItisthecoreprobleminthecomputertheoryandapplicationandhassignificantvalueintheareaofcomputerscience，artificialintelligenceandotherdisciplinesAll—solutionsatisfiabilityproblemhasanimportantapplicationvalueinthefieldofel

3、ectronicdesignautomation(EDA)TllispaperdescribedthesignificanceofAllsolutionBooleansatisfiabilityproblembothintheoreticalandpracticalaspectItcomparedseveralalgorithmsofSATsolversandselectedthealgorithmwithhigherefficienc

4、yandbettersuitabilityforall—solutionSATsolverTwonewalgorithms，intermsofincrementandblockingclause，wereproposedwhichcouldbeappliedtoallsolutionSATsolver(1)Adjustweightofliteralsforincrementalsolving，andconflictanalysisand

5、backtrackingofblockingclausesT11isalgorithmintegratesthevariablestateindependentdecayingsum(VSIDS)decisionheuristicalgorithms，adjusttheweightofliteralsinthebMckingclausesaddedwhiletheall—solutionSATsolverprogramisrunning

6、andthusincreasetheefficiencyofworkingoutallsolutionsAspecialanalysisandbacktrackingmechanismWasproposed，whichcanprocesstheconflictcausedbyblockingclausesandmaketheprogramgotothenextsolvingprocessquicklywhenanewbIockingcl

7、auseWasadded(2)ImprovetheallsolutionSATsolveronbbckingclauseSupplythelikeDon’tcaresalgorithmbasedonCNET11isalgorithmdrawslessonsfromDon’tcaresalgorithmbasedonhybridrepresentations(whichcombinesthecharacteristicsofcircuit

8、withCNF)Tosomeextent，itimprovestheefficiencyofallsolutionSATsolverwhichisbasedonCNFinputMergingtheblockingclauseThisstrategycanmergecurrentblockingclauseswithoutconsumingtoomuchtimeandspaceresourcesTheeffectforimprovingt