cmodels - sat-based disjunctive answer set solver(2)

Disjunctive logic programming under the stable model semantics [GL91] is a new

Ourimplementation–systemCMODELS–usestheprogramLPARSE--dlp-choiceforgroundingdisjunctivelogicprograms.TheinputofCMODELSmayincluderulesofthreetypes.Itallows(i)non-nesteddisjunctiverules,(ii)choicerulesthathavetheform

{A0,...Ak}←Ak+1,...,Al,notAl+1,...,notAm

whereAiareatoms,and(iii)weightconstraintsoftheform

A0←L[A1=w1,...,Am=wm,notAm+1=wm+1,...,notAn=wn](3)(2)whereA0isanatomorsymbol⊥;A1,...,Anareatoms;L(lowerbound);andw1...wn(weights)areintegers.

Theconceptofananswersetforprogramscontainingrules(2)and(3)wasintro-ducedin[NS00].TheoriginalrulesgiventothefrontendLPARSE--dlp-choiceallowlowerandupperboundsforchoicerulesandupperboundsforweightrules.Theyalsoallowuseofliterals(negatedatoms)inplaceofatoms.LPARSE--dlp-choicetranslatesalltherulestotheformsspeci edabove.InCMODELS,choicerulesaretranslatedintonormalnestedrules,andweightconstraintsaretranslatedwiththehelpofauxiliaryvariablesintonormalnon-nestedrules.[FL05]

NotethatCMODELSisthe rstanswersetprogrammingsystemthatallowsuseofdisjunctiveandchoicerulesinthesameprogram.

2DetailsontheModi edAlgorithmsandtheImplementation

Theimplementationisbasedonde nitionsofcompletion,tightnessandloopformulaforDPintroducedin[LL03].Wealsoreferthereaderto[LL03]forformalde nitionsofasetofatomssatisfyingaprogram,answerset,reduct,andpositivedependencygraphofDP.Theimplementationexploitstherelationshipbetweencompletionseman-tics,loopformulasandanswersetsemanticsforDP.Forclassofprogramscalledtightmodelsofcompletionandanswersetsarethesame.Fornontightprogramsthedif-ferenceinsemanticsisduetothecycles(loops)intheprogram.Loopformulasservearoleofanextensiontocompletionsothatthesemanticscoincideagain.Numberofloopformulasisexponentialandthereforeprecomputingallloopformulasatonceisnotfeasible,anditerativeapproachisexplored.ThecorrectnessofalgorithmsencodedinCMODELSfollowsfromtwotheorems.

TheoremforTightPrograms.[LL03]ForanytightDPΠandanysetXofatoms,XisananswersetforΠiffXsatis esprogram’scompletioncomp(Π).

Theorem1.LetΠbeaDP,Mbeamodelofitscompletioncomp(Π),setofatomsM |=ΠM,suchthatM M.TheremustbealoopofΠunderM\M ,s.t.Mdoesnotsatisfyitsloopformula.

Decidingwhetheramodelofthecompletionisananswersetofdisjunctiveprogramisco-NP-complete.WithinthisimplementationofCMODELSweverifythatamodelofthecompletionisindeedananswersetbyusingtheminimalityrequirementofananswerset.WeinvokeaSATsolveronformulaΠM∪M ∪¬M,where(i)ΠMdenotesthereductofΠunderM,s.t.itsrulesarerepresentedaspropositionalformulaswiththecommaunderstoodasconjunction,andA←BasthematerialimplicationB A;