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

CMODELS–SAT-basedDisjunctiveAnswerSetSolver

YuliyaLierler

Erlangen-N¨urnbergUniversit¨at

yuliya.lierler@informatik.uni-erlangen.de

Introduction

Disjunctivelogicprogrammingunderthestablemodelsemantics[GL91]isanewmethodologycalledanswersetprogramming(ASP)forsolvingcombinatorialsearchproblems.Thisprogrammingmethodusesanswersetsolvers,suchasDLV[Lea05],GNT[Jea05],SMODELS[SS05],ASSAT[LZ02],CMODELS[Lie05a].SystemsDLVandGNTaremoregeneralastheyworkwiththeclassofdisjunctivelogicprograms,whileothersystemscoveronlynormalprograms.DLVisuniquelydesignedto ndthean-swersetsfordisjunctivelogicprograms.Ontheotherhand,GNT rstgeneratespossi-blestablemodelcandidatesandthenteststhecandidateontheminimalityusingsystemSMODELSasaninferenceengineforbothtasks.SystemsCMODELSandASSATuseSATsolversassearchengines.Theyarebasedontherelationshipbetweenthecom-pletionsemantics[Cla78],loopformulas[LZ02]andanswersetsemanticsforlogicprograms.HerewepresenttheimplementationofaSAT-basedalgorithmfor ndinganswersetsfordisjunctivelogicprogramswithinCMODELS.Theworkisbasedonthede nitionofcompletionfordisjunctiveprograms[LL03]andthegeneralisationofloopformulas[LZ02]tothecaseofdisjunctiveprograms[LL03].Weproposethenecessarymodi cationstotheSATbasedASSATalgorithm[LZ02]aswellastothegenerateandtestalgorithmfrom[GLM04]inordertoadaptthemtothecaseofdisjunctiveprograms.WeimplementthealgorithmsinCMODELSanddemonstratetheexperimentalresults.1SyntaxofCMODELS

ADisjunctiveprogram(DP)isasetofruleswithexpressionsthathavetheform

A←B,F(1)

whereAistheheadoftheruleandisadisjunctionofatomsorsymbol⊥,Bisaconjunctionofatoms,andFisaformulaofthefollowingform

notA1,...,notAm,notnotAm+1,...,notnotAn

whereAiareatoms.Wecallsuchrulesdisjunctive.Ifaheadofaruledoesnotcontaindisjunction,wecallsucharulenormal.IftheformulaFoftherule(1)containsanexpressionoftheformnotnotAithentheruleisnested,otherwisetheruleisnon-nested.IfallrulesofaDParenormalwecalltheprogramnormal.