计算机科学中的逻辑

《计算机科学中的逻辑》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、LogicinComputerScienceYongmeiLiuymliu@mail.sysu.edu.cnDept.ofComputerScienceSunYat-senUniversityDecember14,2009Y.LiuLogicinComputerScience1/41IntroductionandoutlineFocusonapplicationsoflogicincomputerScience1SATsolversandapplications2Programverication3Modelchecking4CognitiveroboticsY.LiuLogicin

2、ComputerScience2/41AmotivatingexampleWewouldliketoselectpeoplefromAnn,Bob,CarolandDanforacertainjob.Thefollowingconstraintsmustbesatised:BoborCarolshouldbeselectedAnnandDancannotbebothselectedIfBobisselected,DanshouldalsobeselectedHowshouldweselectthepeople?(b_c)^(:a_:d)^(:b_d)fB;DgWhatifwehave

3、manypeopleandmanyconstraints?Y.LiuLogicinComputerScience3/41WhatisSAT?AliteralisanatomorthenegationofanatomAclauseisadisjunctionofliteralsAformulaisinConjunctiveNormalForm(CNF)ifitisaconjunctionofclausesExample:(b_c)^(:a_:d)^(:b_d)SAT:GivenapropositionalformulainCNF,decideifthereexistsatruthassi

4、gnmentthatsatisestheformulaY.LiuLogicinComputerScience4/41TimecomplexityofalgorithmsExpressedintermsofthenumberofoperationsusedDecideifatruthassignmentsatisesaCNFformula:O(m)NaivealgorithmtosolveSAT:O(2nm)n{thenumberofatoms,m{thelengthoftheformulaThecomputertimeusedbyalgorithms*:morethan10100y

5、earsY.LiuLogicinComputerScience5/41Pvs.NPP:theclassofproblemsforwhichthereexistsaprocedurethatrunsinpolynomialtimeO(nb)Example:decideifatruthassignmentsatisesaformulaNP:theclassofproblemswherewearesearchingforaniteminalargespaceofpossibilities,butwherewecantestifacandidateitemisasolutioninpolyn

6、omialtimeExample:decideifapropositionalformulaissatisableP=NP?OneofthesevenMillenniumPrizeProblemsselectedbytheClayMathematicsInstitutetocarryaUS$1,000,000prizefortherstcorrectsolution.ItisgenerallyacceptedthatP6=NPY.LiuLogicinComputerScience6/41NPCompletenessAproblemisNP-completeifitisinNPand

7、anyprobleminNPcanbereducedtoitinpolynomialtimeifanyNP-completeproblemisinP,thenP=NPSATisaclassicalNP-completeproblem,soanyprobleminNPcanbereducedtoSATinpolytimeTherearethousandsofcomputationalproblemsofeconomicsignicancetha