Graphs and colorings for answer set programming

arXiv:cs/0502082v1[cs.AI]21Feb2005UnderconsiderationforpublicationinTheoryandPracticeofLogicProgramming1GraphsandcoloringsforanswersetprogrammingKathrinKonczakandThomasLinkeandTorstenSchaub∗Institutf¨urInformatik,Universit¨atPotsdamPostfach900327,D–14439Potsdam,Germany{konczak,linke,torsten}@cs.uni-potsdam.desubmitted14August2003;revised22July2004;accepted24December2004AbstractWeinvestigatetheusageofruledependencygraphsandtheircoloringsforcharacterizingandcom-putinganswersetsoflogicprograms.Thisapproachprovidesuswithinsightsintotheinterplaybetweenruleswheninducinganswersets.Westartwithdifferentcharacterizationsofanswersetsintermsoftotallycoloreddependencygraphsthatdifferingraph-theoreticalaspects.Wethendevelopaseriesofoperationalcharacterizationsofanswersetsintermsofoperatorsonpartialcolorings.Inanalogytothenotionofaderivationinprooftheory,ouroperationalcharacterizationsareexpressedas(non-deterministicallyformed)sequencesofcolorings,turninganuncoloredgraphintoatotallycoloredone.Inthisway,weobtainanoperationalframeworkinwhichdifferentcombinationsofop-eratorsresultindifferentformalproperties.Amongothers,weidentifythebasicstrategyemployedbythenoMoResystemandjustifyitsalgorithmicapproach.Furthermore,wedistinguishoperationscorrespondingtoFitting’soperatoraswellastowell-foundedsemantics.KEYWORDS:answersetprogramming,operationalsemantics,answersetcomputation,graph-basedcharacterization1IntroductionGraphsconstituteafundamentaltoolwithincomputingscience,inparticular,inprogram-minglanguages,wheregraphsareoftenusedforanalyzingaprogram’sbehavior.Clearly,thisalsoappliestologicprogramming.Forinstance,Prolog’sproceduralsemanticsisin-timatelyconnectedtotheconceptofSLD-trees(Lloyd1987).Forfurtheranalysis,likeprofiling,othertypesofgraphs,suchascallgraphs,playanimportantroleduringpro-gramdevelopment.Similarly,inalternativesemanticsoflogicprogramming,likeanswersetprogramming(GelfondandLifschitz1988;GelfondandLifschitz1991),graphshavebeenusedfordecidingwhetheranswersetsexist(Fages1994;BaralandGelfond1994).Wetaketheapplicationofgraphsevenfurtherandelaborateinthispaperuponanapproachtousinggraphsastheunderlyingcomputationalmodelforcomputinganswersets.Tothisend,webuilduponandlargelyextendthetheoreticalfoundationsintroducedin(Linke2001;Angeretal.2002).Ourapproachhasitsrootsindefaultlogic(Reiter1980),whereextensionsareoftencharacterizedthroughtheir(unique)setofgeneratingdefaultrules.Accordingly,weareinterestedincharacterizinganswersetsbymeansoftheirset∗AffiliatedwiththeSchoolofComputingScienceatSimonFraserUniversity,Burnaby,Canada.2KathrinKonczakandThomasLinkeandTorstenSchaubofgeneratingrules.Fordeterminingwhetherarulebelongstothisset,wemustverifythateachpositivebodyatomisderivableandthatnonegativebodyatomisderivable.Infact,anatomisderivableifthesetofgeneratingrulesincludesarulehavingtheatomasitshead;orconversely,anatomisnotderivableifthereisnoruleamongthegeneratingrulesthathastheatomasitshead.Consequently,theformationofthesetofgeneratingrulesamountstoresolvingpositiveandnegativedependenciesamongrules.Forcapturingthesedependencies,wetakeadvantageoftheconceptofaruledependencygraph,whereineachnoderepresentsaruleoftheunderlyingprogramandtwotypesofedgesstandfortheaforementionedpositiveandnegativeruledependencies,respectively.1Forexpressingtheapplicabilitystatusofrules,thatis,whetherarulebelongstoasetofgeneratingrulesornot,welabel,oraswesaycolor,therespectivenodesinthegraph.Inthisway,ananswersetcanbeexpressedbyatotalcoloringoftheruledependencygraph.Ofcourse,inwhatfollows,wearemainlyinterestedintheinverse,thatis,whendoesagraphcoloringcorre-spondtoananswersetoftheunderlyingprogram;and,inparticular,howcanwecomputesuchatotalcoloring.Generallyspeaking,graphsprovideaformaldeviceformakingstructuralpropertiesofanunderlyingproblemexplicit.Inthisguise,westartbyidentifyinggraphstructuresthatcapturestructuralpropertiesoflogicprogramsandtheiranswersets.Asaresult,weob-tainseveralcharacterizationsofanswersetsintermsoftotallycoloreddependencygraphsthatdifferingraph-theoreticalaspects.Toaturn,webuilduponthesecharacterizationsinordertodevelopanoperationalframeworkforanswersetformation.Theideaistostartfromanuncoloredruledependencygraphandtoemployspecificoperatorsthatturnapartiallycoloredgraphgraduallyintoatotallycoloredonethatrepresentsananswerset.Thisapproachisstronglyinspiredbytheconceptofaderivation,inparticular,bythatofanSLD-derivation(Lloyd1987).Accordingly,aprogramhasacertainanswersetiffthereisasequenceofoperationsturningtheuncoloredgraphintoatotallycoloredonethatprovablycorrespondstotheanswerset.Ourpaperisorganizedasfollows.Section2brieflysummarizesconceptsoflogicpro-gramming.Section3laystheformalfoundationsofourapproachbyintroducingitsbasicgraph-theoreticalinstruments.WhilethefollowingSection4addressescharacterizationsofanswersetsthroughtotallycoloredgraphs,Section5dealswithoperationalcharacter-izationsofanswersets.Section6identifiesrelationshipswithFitting’sandwell-foundedsemantics.Section7discussestheapproach,inparticularinthelightofrelatedwork.Weconcl