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

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

instance

SAT

SAT

SAT

qbf1

qbf2

qbf3

qbf4dlv.5.02.230.01(23)0.01(23)0.01(33)19.815.435.276.83cmodels+zchaff0.14(5)0.09(4)0.09(5)0.01(16)823.98(19928)1779.28(28481)10.55(137)gnt20.0011466.30--

Fig.1.CMODELSusingMCHAFF,ZCHAFF,SIMOvs.DLV,andGNTon2QBFbenchmark3ExperimentalAnalyses

DetailsontheperformanceofsystemCMODELSincaseoftightdisjunctiveprogramscanbefoundin[Lie05b].ForexperimentalanalysisofCMODELS’performanceonnon-tightprogramsweshallspecifythealgorithmicdifferencesofSATsolvers’invocations.AlgorithmDP-assat-ProcisimplementedinCMODELSusingSATsolverMCHAFF1inStep2.AlgorithmDP-generate-test-enhanced-ProcisimplementedinCMODELSwithSATsolverSIMO2orZCHAFF1invokedinplaceofSAT-Aintheprocedure.IncaseofDP-generate-test-enhanced-ProcimplementationofStep6whencontrolisgivenbacktotheSATsolver,SIMOandZCHAFFbehavedifferently.SIMOcontinuesitsworkwiththesamesearchtreeitobtainedinpreviouscomputations,whileZCHAFFstartsbuildinganewsearchtree.InallcasesZCHAFFisusedforminimalitytestprocedure.pThe rstexperimentthatwedemonstrateis2QBFbenchmark.TheproblemisΣ2-hard.Theencodingandtheinstancesoftheproblemwhereobtainedattheweb-siteoftheUniversityofKentucky3.Figure1presentstheresults.TheexperimentswererunonPentium4,CPU3.00GHz.Thecolumns3through7presenttherunningtimesofthesystemsinsecondswith30minutescutofftime.Numberinparenthesesspeci eshowoftenCMODELSinvokedtheminimalitytestprocedureduringitsrun.Incaseofsatis ableinstancesoftheproblemwecanseethepayoffinusingCMODELSinplaceofotherdisjunctiveASPsolvers.Thepicturechangeswhenunsatis ableinstancesoftheproblemcomeintoplay.ImplementationofDP-assat-Procreachestimelimittwiceandincaseofoneinstancereachesthememorylimit.ImplementationofDP-generate-test-enhanced-ProcshowsbetterresultsbutasaruleisslowerthanDLVrunningtimebytwoordersofmagnitude.Ifwepayattentiontothenumberofminimalitytestproce-dureinvocations,theslowperformanceisnotsurprising.Thenumberofmodelsofthecompletionislargeincaseofunsatis ableinstancesqbf2,qbf3instancesandhenceallfoundmodelsmustbeveri edanddeniedbytheminimalitytestprocedure.

ThesecondexperimentthatwepresentistheStrategicCompanybenchmark.ThepproblemisΣ2-hard.Weusedtheencodingandtheinstancesoftheproblemprovidedbythebenchmarksystemforanswersetprogramming–Asparagus4.Figure2presents