; TeX output 1999.04.28:1500 LfT rhtml: html:L[Dt G G cmr17The7tComplexitqyofPosorMan'sLogiclύ XQ cmr12EdithHemaspaandra(lύ l/"V
cmbx10Abstractٜ/sK`y
cmr10Motivqatedbydescriptionlogics,weinvestigatewhathappGenstothecomplexity
rofmoGdalsatisabilityproblemsifweonlyallowformulasbuiltfromliterals,*
!",
cmsy10^,Tq
lasy103, randn2.Previously*,t,theonlyknownresultwasthatthecomplexityofthesatisability rproblemzforK~droppGedfromPSP*ACE-completetocoNP-complete(Schmidt-Schauss rand9Smolkqa[html:5 html: ]andDoninietal.[html:2 html:]).hInthispapGerweshowthatnotalllogicsbGehave rlikeK.#PInparticular, weshowthatthecomplexityofthesatisabilityproblemwith rrespGect7toframesinwhicheachworldhasatleastonesuccessordropsfromPSP*ACE- rcompleteTtoP*,butthatincontrastthesatisabilityproblemwithrespGecttotheclass rofQframesinwhicheachworldhasatmosttwosuccessorsremainsPSP*ACE-complete. rAsacorollaryofthelatterresult,wealsosolvetheonemissingcasefromDoniniet ral.'sUUcomplexityclassicationofdescriptionlogics[html:1 html: ]."A r!N ff cmbx12Contentsύ rhtml:""V
3
cmbx101lInttroYduction html:.2 rhtml:2lPtoYor2Man'sV\ersionsofNP-completeSatisabilityProblems html:3 rhtml:3lPtoYorMan'sV\ersionsofPSPAtCE-completeSatisabilityProb-
0Alems html:HZ84 rhtml:4l$!",
3
cmsy10ALE N6FVSatisabilitty2isPSP\ACE-complete html:~79 ٯK`y
3
cmr101 *LfT rhtml: html: rfThtml: html: 1LIntros3ductionqSinceconsisten!tnormalmoMdallogicscontainpropMositionallogic,5thesatisabil-
it!yproblemsforalltheselogicsareautomaticallyNP-hard.Infact,asshownb!yfLadner[html:4 html:y],manyofthemareevenPSPeACE-hard. Butw!edon'talwaysneedallofpropMositionallogic."Feorexample,-insomeapplications[w!emaybMeabletoboundthen!umber[ofpropositionalvdDariables.PropMositional%satisabilit!ythusrestrictedisinPe,and,?asshownbyHalpMern[html:3 html:y],thePcomplexit!yofsatisabilityproblemsforsomemoMdallogicsrestrictedinthesameTQw!ayalsodecreases.Feorexample,dthecomplexityofS57satisabilitydropsfrom7NP-completetoPe.Ontheotherhand,lKsatisabilit!yremainsPSPA!CE-complete. Restrictingmthen!umbMermofpropositionalvdDariablesisnottheonlyproposi-tionalIrestrictiononmoMdallogicsthatoccursintheliterature.~Feorexample,OthedescriptionlogicALE5]canbMeview!edasmulti-moMdalKwheretheonlyallowedpropMositionalyoperatorsare:onpropositionalvdDariablesand^.BothmodalopMeratorsf%Tq
3
lasy102and3areallo!wed. As~inthecaseofaxedn!umbMer~ofpropositionalvdDariables,satisabilit!yforpropMositionalIVlogicwithonly:onpropositionalvdDariablesand^asoperatorsisinPe.Afterall,5inthatcaseev!erypropMositionalformulaistheconjunctionoffliterals.Suc!haformulaissatisableifandonlyifthereisnopropMositionalvdDariablef#b>
3
cmmi10psuc!hthatbMothpand:pareconjunctsoftheformula. Satisabilit!y*dformoMdallogicswhoseoperatorsarerestrictedinthisw!ayis2notautomaticallyNP-hard.@Ofcourse,itdoMesnotnecessarilyfollo!wthattheDcomplexit!yofmoMdalsatisabilityproblemswilldropsignicantlye. Theonlys@resultthatw!aspreviouslyknownisthatthecomplexityofKjsatisabilitydrops
TfromPSPeA!CE-completetocoNP-complete.TheuppMerboundw!asshownb!ySchmidt-SchaussandSmolkdDa[html:5 html:y],andthelowerbMoundbyDoninietal.[html:2 html:y].IteshouldbMenotedthattheseresultsw!ereshowninthecontextofdescriptionlogics,fsothatthenotationinthesepapMersisquitedieren!tfromours. InthispapMerw!einvestigateifitisalwaysthecasethatthecomplexityofthecXsatisabilit!yproblemdecreasesifweonlyloMokatformulasthatarebuiltfromliterals,^,3,and2,andifso,ifthereareuppMerorlo!werbMoundsontheamoun!tfthatthecomplexitydrops. Wee%willsho!wthatnotalllogicsbMehavelikeKk.EFearfromit,<byloMokingatsimpleAKrestrictionsonthen!umbMerAKofsuccessorsthatareallo!wedAKforeac!hworld,w!efobtainmanydierentbMehaviors.Inparticular,wewillshowthathtml: html:
x
-1.Thecomplexit!yofthesatisabilityproblemwithrespMecttolinearframesdropsffromNP-completetoPe.!html: html:
-2.TheMcomplexit!yofthesatisabilityproblemwithrespMectto <