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

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

(ii)M denotestheconjunctionofnegationoftheatomsinΠthatdonotbelongtoM;and(iii)¬MdenotesthenegationoftheconjunctionofatomsinM.Ifthisformulaisunsatis edthenMisindeedananswersetofΠotherwisesomemodelM Misreturned.NotethatM |=Π.Wecallthisprocedureminimalitytest.Itissimilartotheprocedureintroducedin[JNSY00].[KLP03]introducedamoresophisticatedwayofverifyingwhetheramodelisananswersetusingSATsolversbyexploitingsomemodularitypropertyoftheprogram,thatpermitssplittingveri cationsteponthewholeprogramintoveri cationonitsparts.Itisadirectionoffutureworktoresearchtheapplicabilityoftheapproachtothecaseofnestedprograms.

CMODELS’algorithmisenhancedtoverifythetightnessofDPat rst.IncasewhenaprogramistightitperformsacompletionprocedureontheprogramandusesaSATsolverforenumeratingitsanswersets,avoidinginvocationofminimalitytestproce-dure.Thiswayweallowef cientuseofSATsolversinASP,byanalysingprogramsyntacticallyandidentifyinginadvancedisjunctiveprograminvolvinglowercomputa-tionalcomplexity.

FornontightprogramsweadaptASSATalgorithm[LZ02]tothecaseofdisjunctiveprogramsbasedonTheorem2.Themodi edalgorithmfollows—DP-assat-Proc:1LetTbetheCompletionofΠ—Comp(Π)

2InvokeSATsolverSAT-Ato ndamodelMofT.Ifthereisnosuchmodelthenterminatewithfailure.

3InvoketheminimalitytestprocedureonprogramΠ,andmodelMwithSATsolverSAT-Bto ndmodelM .IfthereisnosuchmodelthenexitwithananswersetM.IfthereisamodelM thenMisnotananswersetofΠ.

4BuildthesubgraphGM\M ofthepositivedependencygraphofΠinducedbyM\M .LookforloopLinGM\M ,s.t.M|=FL,whereFLisaloopformulaofL.

5LetTbeT∪FL,andgobacktostep2.

TheimplementationalsoadaptsanotherSAT-basedanswersetprogramminggen-erateandtestalgorithmfrom[GLM04]tothecaseofnontightdisjunctiveprograms.State-of-the-artSATsolversareenhancedbytheabilityofperformingbackjumpingandlearningwithinstandardSATDavis-Logemann-Loveland(DLL)procedure.Back-jumpingandlearningtechniquesareduetoprovidingDLLprocedurewithacertainclause.WeretrievethenecessaryclausefromsomeloopformulaofaprogramthatallowsustoenhanceSATsolverinnercomputation.TheenhancedgenerateandtestalgorithmforDP—DP-generate-test-enhanced-Proc:

1ComputecompletionofΠ—Comp(Π)

2InitiateSATsolverSAT-AwiththecompletionComp(Π).InvokeDLLto ndmodelMofComp(Π).Ifthereisnosuchmodelthenterminatewithfailure.3,4ThesameasStep3,4ofDP-assat-proc.

5CalculateaclauseClimpliedbyFLsuchthatM|=Cl.

6ReturncontroltotheSAT-AprocedureDLLbygivingClasaclausetobackjumpandlearn.FindthenextmodelMofthecompletion.Ifthereisnosuchmodelthenterminatewithfailure.Gobacktostep3.