Logic Programming under the Stable Model Semantics

ABackjumpingTechnique

forDisjunctiveLogicProgramming

FrancescoRicca∗,WolfgangFaberandNicolaLeone

DepartmentofMathematics,UniversityofCalabria.87030Rende(CS),Italy

E-mail:{ricca,faber,leone}@mat.unical.it

InthisworkwepresentabackjumpingtechniqueforDis-junctiveLogicProgrammingundertheStableModelSeman-tics(SDLP).Itbuildsuponrelatedtechniquesthathadorigi-nallybeenintroducedforconstraintsolving,whichhavebeenadaptedtopropositionalsatisfiabilitytesting,andrecentlyalsotonon-disjunctivelogicprogrammingunderthestablemodelsemantics(SLP)[1,2].

Wefocusonbackjumpingwithoutclauselearning,provid-inganewtheoreticalframeworkforbackjumpinginSDLP,elaboratingonandexploitingpeculiaritiesofthedisjunctivesetting.Wepresentareasoncalculusandassociatedcompu-tations,which–comparedtothetraditionalapproaches–re-ducestheinformationtobestored,whilefullypreservingthecorrectnessandtheefficiencyofthebackjumpingtechnique,handlingspecificaspectsofdisjunctioninabenignway.WeimplementedtheproposedtechniqueinDLV,thestate-of-the-artSDLPsystem.

Wehaveconductedseveralexperimentsonhardrandomandstructuredinstancesinordertoassesstheimpactofbackjumping.Tothisend,wehavecomparedDLVinvar-iousversions:Withandwithoutthebackjumpingmethoddescribedinthispaper,incombinationwithtwodifferentheuristicfunctions.Ourconclusionisthatunderanyoftheheuristicfunctions,DLVwithbackjumpingisfavourabletoDLVwithoutbackjumping.DLVwithbackjumpingper-formsparticularlywellonstructuredsatisfiabilityandquan-tifiedbooleanformulainstances,wherethesearchspaceandexecutiontimeareeffectivelycut.

Keywords:LogicProgramming,StableModels,Backjump-ing,Experiments

AICommunications

ISSN0921-7126,IOSPress.Allrightsreserved

1Often

SDLPisreferredtoasAnswerSetProgramming(ASP).

WhileASPsupportsalsoasecond(“strong”)kindofnegation,itcanbesimulatedinSDLP.Toavoidconfusion,wewillonlyusethetermSDLPinthispaper.

2F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

Thefirsttwolinesintroducesuitablefacts,represent-ingG,thethirdlinestatesthateachvertexneedstohavesomecolor.Sincestablemodelsareminimalw.r.t.setinclusion,eachvertexwillbeassociatedtopre-ciselyonecolorinanystablemodel.Thelastlineactsasanintegrityconstraintanddisallowssituationsinwhichtwoverticesconnectedbyanedgeareassociatedwiththesamecolor.Bynow,severalsystemsareavail-able,whichimplementSDLP:DLV[9],GnT[10],andrecentlycmodels-3[11].

MainIssues.Mostoftheoptimizationworkonre-latedSDLPsystemshasfocusedontheefficienteval-uationofnon-disjunctiveprograms(whosepowerislimitedtoNP/co-NP),whereastheoptimizationoffullSDLPhasbeentreatedinfewerworks(e.g.,in[10,12]).

Oneofthemorerecentproposalsforenhancingtheevaluationofnon-disjunctiveprogramshasbeenthedefinitionofbackjumpingandclauselearningmechanisms.ThesetechniqueshadbeensuccessfullyemployedinCSPsolvers[13,14]andpropositionalSATsolvers[15,16]before,andwere“ported”tonon-disjunctivelogicprogrammingunderthestablemodelsemantics(SLP)in[1,2],resultinginthesystemSmodelscc.

Inthispaperweaddresstwoquestions:

◮Howcanbackjumpingbegeneralizedtodisjunctiveprograms?

◮Isbackjumpingwithoutclauselearningeffective?WhyBackjumping?Asforanintuitionaboutthevalueofbackjumping,considerthefollowinginstanceofthe3COLORABILITYproblem:

abecdNotethatvertexeisnotonanyedge.

edge(a,b).edge(a,c).edge(a,d).edge(b,d).edge(c,b).edge(c,d).vertex(a).vertex(b).vertex(c).vertex(d).vertex(e).

Informally,anevaluationcouldnowproceedasfol-lows,2assketchedinFig.1.First,assumecol(a,red)tohold.Asaconsequencecol(b,red),col(c,red),col(d,red)mustbefalse(otherwisetheintegritycon-

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming3

cometrueorfalseatsomepoint,triggeringthesamecontradictions.Thereforewecanbackjumptotheclos-estreasonoftheinconsistentsubtree.

Insum,oncetheaboveinconsistencyarises,anal-gorithmbasedon(chronological)backtracking,triesthecomplementofthesecondchoice(col(e,green)),makingfurtherchoicesandalotofuselesscomputa-tionsallleadingtotheinconsistenciesencounteredbe-fore.Backjumping,instead,allowsustojumpdirectlytothesourceoftheinconsistency(col(a,red)),reduc-ingthesearchspacesignificantly.

Contributions.Backjumpingnotionshavefirstbeenstudiedforconstraintsolving,havebeenappliedsuc-cessfullyforSATsolvingandhaverecentlybeenportedtoSLPin[1,2].InthispaperwefirstpresentageneralizationoftheseapproachestodisjunctiveprogramsbydefiningareasoncalculusfortheDet-ConsfunctionofDLV(whichroughlycorrespondstounitpropagationinDPLL-basedSATsolversandAtLeast/AtMostinSmodels).Thesereasonscanthenbeexploitedforeffectivebackjumping.Specialatten-tionispaidtopeculiaritiesofthedisjunctivesetting.Wealsodescribetheimplementationofthesetech-niquesintheDLVsystem,thestate-of-the-artSDLPsystem.Infact,ourimplementationaimsatreducingtheinformationtobestoredasmuchaspossible,whilemaintainingthebestjumpingpossibilities.

Subsequently,weassessourmethodandimplemen-tationbyanexperimentationactivity.Wehavetestedtheimpactofbackjumpingbothwithandwithouttheemploymentofthelookahead(seeSection5),onran-dom3SATinstances,ΣP2-hardQBF,andsomestruc-turedSATinstances.

Thefullpictureresultingfromtheexperimentsisverypositive:

–OnSigmaP2-hardQBF,theBackjumpingtech-nique(BJ)reducesthenumberofchoicepointssignificantly.Suchareductionimpliesalsorele-vanttime-gainsintheprogramevaluation.Boththereductionofchoicepointsandthetime-gainareobservedeveniflookaheadisemployed.

–Thebackjumpingtechniquehasapositiveim-pactalsoontheevaluationofstructured3SATin-stances.Choicepointsarereducessensibly,andatime-gainisobtained,bothwithandwithoutthelookahead.

–Onrandom3SATinstances,thebackjumpingtechniquebringsareductionofthesearchspace(fewerchoicepoints),iflookaheadisnotem-ployed.Thisreductioniscompensatedbythe

overheadbroughtbythereasoncalculus,butsuchanoverheaddoesnotovercomethegain:thetwoversions(with/withoutbackjumping)essentiallyshowthesameperformance.Iflookaheadisem-ployed,thereisnocutofthesearchspaceinthiscase;buttheoverheadincomputation-time,whichisbroughtbythereasoncalculus,isnegli-gible.

Insum,theresultsoftheexperimentsletusconcludethefollowing:

–Backjumpingispreferabletotheversionwithoutbackjumping,independentlyoftheheuristicem-ployedinDLV.

–Backjumpingwithoutclauselearningcanbeef-fective.

–Evenincases,inwhichthesearchspaceisnotprunedbybackjumping,theoverheadisnegligi-ble.

Theorganizationofthepaperisasfollows.InSec-tion2wereviewthesyntaxandsemanticsofSDLP,andrecallsomeofitsproperties.InSection3,thecom-putationalcoreofDLVispresented,whichisextendedinSection4byasuitablebackjumpingmethod.InSection5wereportonthebenchmarksperformedtoassestheimpactofthisbackjumpingmethod.Finally,inSection6wedrawoutconclusionsandoutlinefu-turework.

2.DisjunctiveLogicProgramming

Inthissection,weprovideabriefintroductiontothesyntaxandsemanticsofDisjunctiveLogicProgram-ming;forfurtherbackgroundsee[17,18].2.1.Syntax

Adisjunctiverulerisaformula

a1v···van:-b1,···,bk,notbk+1,···,notbm.wherea1,···,an,b1,···,bmareatoms3andn≥0,m≥k≥0.Aliteraliseitheranatomaoritsdefaultnegationnota.Givenaruler,letH(r)={a1,...,an}denotethesetofheadliterals,B+(r)={b1,...,bk}andB−(r)={notbk+1,...,notbm}thesetofpos-

4F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

itiveandnegativebodyliterals,resp.,andB(r)=B+(r)∪B−(r).thesetofbodyliterals.

ArulerwithB−(r)=∅iscalledpositive;arulewithH(r)=∅isreferredtoasintegrityconstraint.Ifthebodyisemptyweusuallyomitthe:-sign.

AdisjunctivelogicprogramPisafinitesetofrules;PisapositiveprogramifallrulesinParepositive(i.e.,not-free).Anobject(atom,rule,etc.)containingnovariablesiscalledgroundorpropositional.

Givenaliterall,letnot.l=aifl=nota,oth-erwisenot.l=notl,andgivenasetLofliterals,not.L={not.l|l∈L}.

Forexampleconsiderthefollowingprogram:r1:a(X)vb(X):-c(X,Y),d(Y),note(X).r2::-c(X,Y),k(Y),e(X),notb(X)r3:m:-n,o,a(1).r4

:

c(1,2).

r1isadisjunctiverules.t.H(r1)={a(X),b(X)},B+(r1)={c(X,Y),d(Y)},andB−(r1)={e(X)};r2isaconstraints.t.B+(r2)={c(X,Y),k(Y),e(X)},andB−(r2)={b(X)};r3isagroundpositive(non-disjunctive)rules.t.H(r3)={m}B+(r3)={n,o,a(1)},andB−(r3)=∅;r4isafact(notethat:-isomitted).2.2.Semantics

Thesemanticsofadisjunctivelogicprogramisgivenbyitsstablemodels[19],whichwebrieflyre-viewinthissection.

GivenaprogramP,lettheHerbrandUniverseUPbethesetofallconstantsappearinginPandtheHer-brandBaseBPbethesetofallpossiblegroundatomswhichcanbeconstructedfromthepredicatesymbolsappearinginPwiththeconstantsofUP.

Givenaruler,Ground(r)denotesthesetofrulesobtainedbyapplyingallpossiblesubstitutionsσfromthevariablesinrtoelementsofUP.Similarly,givenaprogram󰀂

P,thegroundinstantiationPofPisthesetrFor∈PGround(r).

everyprogramP,wedefineitsstablemodelsusingitsgroundinstantiationPintwosteps:Firstwedefinethestablemodelsofpositiveprograms,thenwegiveareductionofgeneralprogramstopositiveonesandusethisreductiontodefinestablemodelsofgen-eralprograms.

AsetLofgroundliteralsissaidtobeconsistentif,foreveryatomℓ∈L,itscomplementaryliteralnotℓisnotcontainedinL.AninterpretationIforPisa

consistentsetofgroundliteralsoveratomsinBP.4Agroundliteralℓistruew.r.t.Iifℓ∈I;ℓisfalsew.r.t.IifitscomplementaryliteralisinI;ℓisundefinedw.r.t.Iifitisneithertruenorfalsew.r.t.I.

LetrbeagroundruleinP.Theheadofristruew.r.t.Iifexistsa∈H(r)s.t.aistruew.r.t.I(i.e.,someatominH(r)istruew.r.t.I).Thebodyofristruew.r.t.Iif∀ℓ∈B(r),ℓistruew.r.t.I(i.e.allliteralsonB(r)aretruew.r.tI).Thebodyofrisfalsew.r.t.Iif∃ℓ∈B(r)s.t.ℓisfalsew.r.tI(i.e.,someliteralinB(r)isfalsew.r.t.I).Therulerissatisfied(ortrue)w.r.t.Iifitsheadistruew.r.t.Ioritsbodyisfalsew.r.t.I.

InterpretationIistotalif,foreachatomAinBP,eitherAornot.AisinI(i.e.,noatominBPisunde-finedw.r.t.I).AtotalinterpretationMisamodelforPif,foreveryr∈P,atleastoneliteralintheheadistruew.r.t.Mwheneverallliteralsinthebodyaretruew.r.t.M.XisastablemodelforapositiveprogramPifitspositivepartisminimalw.r.t.setinclusionamongthemodelsofP.

Forexample,considerthepositiveprograms

P1={avbvc.;:-a.}

P2={avbvc.;:-a.;b:-c.;c:-b.}ThestablemodelsofP1are{b,nota,notc}and{c,nota,notb},while{b,c,nota}istheonlystablemodelofP2.

ThereductorGelfond-Lifschitztransformofagen-eralgroundprogramPw.r.t.aninterpretationXisthepositivegroundprogramPX,obtainedfromPby(i)deletingallrulesr∈Pwhosenegativebodyisfalsew.r.t.Xand(ii)deletingthenegativebodyfromtheremainingrules.

AstablemodelofageneralprogramPisamodelXofPsuchthatXisastablemodelofPX.Giventhe(general)program

P3={

avb:-c.;

b:-nota,notc.;avc:-notb.}

andtheinterpretationI={b,nota,notc},thereductP3Iis{avb:-c.,b.}.IisastablemodelofPIthisreasonitisalsoastablemodelofP3,andfor3.Now

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming5

considerJ={a,notb,notc}.ThereductP3

Jis{avb:-c.;avc.}anditcanbeeasilyverifiedthat

JisastablemodelofP3J

,soitisalsoastablemodelofP3.

2.3.SomeSDLPProperties

GivenaninterpretationIforagroundprogramP,wesaythatagroundatomAissupportedinIifthereexistsasupportingruler∈ground(P),i.e.thebodyofristruew.r.t.IandAistheonlytrueatomintheheadofr.IfMisastablemodelofaprogramP,thenallatomsinMaresupported[20,21,22].

Animportantpropertyofstablemodelsisrelatedtothenotionofunfoundedset[23,21].LetIbea(partial)interpretationforagroundprogramP.AsetX⊆BPofgroundatomsisanunfoundedsetforPw.r.t.Iif,foreacha∈Xandforeachruler∈Psuchthata∈H(r),atleastoneofthefollowingconditionsholds:(i)B(r)∩not.I=∅,(ii)B+(r)∩X=∅,(iii)(H(r)−X)∩I=∅.

LetIPdenotethesetofallinterpretationsofPforwhichtheunionofallunfoundedsetsforPw.r.t.IisanunfoundedsetforPw.r.t.Iaswell5.GivenI∈IP,letGUSP(I)(thegreatestunfoundedsetofPw.r.t.I)denotetheunionofallunfoundedsetsforPw.r.t.I.IfMisatotalinterpretationforaprogramP.MisastablemodelofPiffnot.M=GUSP(I)[21].

WitheverygroundprogramP,weassociateadi-rectedgraphDGP=(N,E),calledthedependencygraphofP,inwhich(i)eachatomofPisanodeinNand(ii)thereisanarcinEdirectedfromanodeatoanodebiffthereisarulerinPsuchthatbandaappearintheheadandpositivebodyofr,respectively.

ThegraphDGPsinglesoutthedependenciesoftheheadatomsofarulerfromthepositiveatomsinitsbody.6

Asanexample,considertheprograms

P4={avb.;c:-a.;c:-b.}

P5=P4∪{dve:-a.;d:-e.;e:-d,notb.}.ThedependencygraphDGP4ofP4isdepictedinFigure2(a),whilethedependencygraphDGP5ofP5isdepictedinFigure2(b).

c-ca󰀒Ib

a6󰀒Ib

(a)

Fig.2.Graphs(a)DGP4,and(b)DGP5

AprogramPishead-cycle-free(HCF)iffthereisno

rulerinPsuchthattwoatomsoccurringintheheadofrareinthesamecycleofDGP[24].

Consideringthepreviousexample,thedependencygraphsgiveninFigure2revealthatprogramP4isHCFandthatprogramP5isnotHCF,asruledve:-a.con-tainsinitsheadtwoatomsbelongingtothesamecycleofDGP5.

AcomponentCofadependencygraphDGisamaximalsubgraphofDGsuchthateachnodeinCisreachablefromanyother.ThesubprogramofCcon-sistsofallruleshavingsomeatomfromCinthehead.Anatomisnon-HCFifthesubprogramofitscompo-nentisnon-HCF.

3.ModelGenerationinDLV

Inthissection,webrieflydescribethecomputationalprocessperformedbytheDLVsystem[21,25]tocom-putestablemodels,whichwillbeusedfortheexper-iments.Notethat,otherSDLPandSLPsystemslikeSmodels[26,27]employaverysimilarprocedure.Ingeneral,alogicprogramPcontainsvariables.ThecomputationalstepofanSDLPsystemelimi-natesthesevariables,generatingagroundinstantiationground(P)ofPwhichisa(usuallymuchsmaller)subsetofallsyntacticallyconstructibleinstancesoftherulesofPhavingpreciselythesamestablemodelsasP[28].

3.1.MainModelGenerationProcedure

ThenondeterministicpartofthecomputationisperformedonthissimplifiedgroundprogrambytheModelGenerator,whichissketchedbelow.Notethatforreasonsofpresentation,thedescriptionhereisquitesimplified;inparticular,thechoicepointsandsearchtreesaresomewhatmorecomplexinthe“real”imple-mentation.However,onecanfindaone-to-onemap-pingtothesimplerformalismdescribedhere.Amoredetaileddescriptioncanbefoundin[25].Notealsothattheversiondescribedherecomputesonestablemodelforsimplicity,howevermodifyingittocomputeallornstablemodelsisstraightforward.Forbrevity,Preferstothesimplifiedgroundprograminthesequel.

6F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

boolMG(Interpretation&I){

if(!DetCons(I))thenreturnfalse;

if(“noatomisundefinedinI”)thenreturnIsUnfoundedFree(I);SelectanundefinedatomAusingaheuristic;if(MG(I∪{A})thenreturntrue;elsereturnMG(I∪{notA});};

Fig.3.ComputationofStableModels

Roughly,theModelGeneratorproducessome“can-didate”stablemodels.EachcandidateIisthenveri-fiedbythefunctionIsUnfoundedFree(I),whichcheckswhetherIisaminimalmodeloftheprogramPIob-tainedbyapplyingtheGL-transformationw.r.t.I.Thispartofthecomputationisalsoreferredtoasmodelorstabilitychecker.

TheinterpretationshandledbytheModelGenera-torarepartialinterpretations.Initially,theMGfunc-tionisinvokedwithIsettotheemptyinterpretation(allatomsareundefinedatthisstage).IftheprogramPhasastablemodel,thenthefunctionreturnstrueandsetsItothecomputedstablemodel;otherwiseitreturnsfalse.TheModelGeneratorissimilartotheDavis-PutnamprocedureinSATsolvers.ItfirstcallsafunctionDetCons,whichextendsIwiththoseliteralsthatcanbedeterministicallyinferred.ThisissimilartounitpropagationasemployedbySATsolvers,butex-ploitsthepeculiaritiesofSDLPformakingfurtherin-ferences(e.g.,itusestheknowledgethateverystablemodelisaminimalmodel).

DetCons(I)computesthedeterministicconsequencesofI,andwillbedescribedinmoredetailinSection3.2.IfDetCons(I)doesnotdetectanyinconsistency,anatomAisselectedaccordingtoaheuristiccriterionandMGisrecursivelycalledonbothI∪{A}andI∪{notA}.TheatomAcorrespondstoabranchingvariableinSATsolvers.

Theefficiencyofthewholeprocessdependsontwocrucialfeatures:agoodheuristictochoosethebranch-ingvariablesandanefficientimplementationofDet-Cons.Actually,theDLVsystememploysbydefaultasocalledlookaheadheuristic[29,30]andanefficientDetConsimplementation[31,32].

Inalookaheadheuristic,eachpossiblechoicelit-eralistentativelyassumed,itsconsequencesarecom-puted,andsomecharacteristicvaluesontheresultarerecorded.Basedonthesevalues,thechoiceisdeter-mined.Wewillnotdescribethemethodherefurther,asitisnotconnectedtobackjumping,andreferto[29,30]fordetails.

Itisworthnotingthat,ifduringtheexecutionoftheMGfunctionacontradictionarises,orthestablemodel

candidateisnotaminimalmodel,MGbacktracksandmodifiesthelastchoice.Thiskindofbacktrackingiscalledchronologicalbacktracking.

InSection4,wedescribeatechniqueinwhichthetruthvalueassignmentscausingaconflictareidenti-fiedandbacktrackingisperformed“jumping”directlytoapointsothatatleastoneofthoseassignmentsismodified.Thiskindofbacktrackingtechniqueiscallednon-chronologicalbacktrackingorbackjumping.3.2.DetCons

Aspreviouslypointedout,theroleofDetConsissimilartotheBooleanConstraintPropagation(BCP,oftenreferredtoasunitpropagation)procedureinDavis-PutnamSATsolvers.However,DetConsismorecomplexthanBCP,whichisbasedonthesimpleunitpropagationinferencerule,whileDetConsimplementsasetofinferencerules.Thoserulescombineanexten-sionoftheWell-foundedoperatorfordisjunctivepro-gramswithanumberoftechniquesbasedonSDLPprogramproperties.Wewillnotdefinetheserulesortheirimplementationindetailhere,astheyarenotanoveltyofthispaper,andreferto[31,32]fortheirpre-cisedefinitionsandimplementation.

WhilethefullimplementationofDetConsinvolvesfourtruthvalues(apartfromtrue,false,andundefined,thereisalso“mustbetrue”),wetreat“mustbetrue”astrueinthisdescriptionforsimplicity,astheyaretreatedinthesamewaywithrespecttobackjumping.Moreover,wegrouptheinferencerulesusingthesameterminologyas[1]forbettercomparability:1.ForwardInference,

2.Kripke-KleeneNegation,

3.ContrapositionforTrueHeads,4.ContrapositionforFalseHeads,5.

Well-foundedNegation.

Rule1derivesanatomastrueifitoccursintheheadofaruleinwhichallotherheadatomsarefalseandthebodyistrue.Rule2derivesanatomasfalseifnorulecansupportit.Rule3appliesifforatrueatomonlyonerulethatcansupportitisleft,andmakesinferencessuchthattherulecansupporttheatom,i.e.derivesallotherheadatomsasfalse,atomsinthepositivebodyastrueandatomsinthenegativebodyasfalse.Rule4makesinferencesforruleswhichhaveafalsehead:Ifonlyonebodyliteralisundefined,deriveatruthvalueforitsuchthatthebodybecomesfalse.Finally,rule5setsallmembersofthegreatestunfoundedsettofalse.Wenotethatrule5isonlyappliedonrecursiveHCFsubprogramsforcomplexityreasons[32].

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming7

4.Backjumping

Inthissectionwefirstmotivatebymeansofanex-amplehowabackjumpingtechniqueissupposedtowork,andthengiveamoreformalaccountonhowtoextendthefunctionsDetConsandMGofDLVtoac-complishthistaskingeneral.4.1.BackjumpingbyExampleConsiderthefollowingprogramr1:avb.r2:cvd.r3:evf.r4:g:-a,e.r5::-g,a,e.r6:g:-a,f.r7::-g,a,f.

andsupposethatthesearchtreeisasdepictedinFig.4.

Fig.4.BacktrackingvsBackjumping.

Accordingtothistree,wefirstassumeatobetrue,derivingbtobefalse(becauseofr1andrule3).Thenweassumectobetrue,derivingdtobefalse(becauseofr2andrule3).Third,weassumeetobetrueandderiveftobefalse(becauseofr3andrule3)andgtobetrue(becauseofr4andrule1).Thistruthassign-mentviolatesconstraintr5(becauserule4derivesgtobefalse),yieldinganinconsistency.Wecontinuethesearchbyinvertingthelastchoice,thatis,weassumeetobefalseandwederiveftobetrue(becauseofr3andrule1)andgtobetrue(becauseofr7andrule1),butobtainanotherinconsistency(becauseofconstraintr7andrule4,gmustalsobefalse).

Atthispoint,MGgoesbacktothepreviouschoicepoint,inthiscaseinvertingthetruthvalueofc(cf.thearclabelledBKinFig.4).

Nowitisimportanttonotethattheinconsistenciesobtainedareindependentofthechoiceofc,andonlythetruthvalueofaandearethe“reasons”fortheen-counteredinconsistencies.Infact,nomatterwhatthetruthvalueofcis,ifaistruethenanytruthassignmentforewillleadtoaninconsistency.LookingatFig.4,thismeansthatinthewholesubtreebelowthearcla-belledanostablemodelcanbefound.Itisthereforeobviousthatthechronologicalbacktrackingsearchex-ploresbranchesofthesearchtreethatcannotcontainastablemodel,performingalotofuselesswork.

Abetterpolicywouldbetogobackdirectlytothepointatwhichweassumedatobetrue(seethearclabelledBJinFig.4).Inotherwords,ifweknowthe“reasons”ofaninconsistency,wecanbackjumpdi-rectlytotheclosestchoicethatcausedtheinconsistentsubtree.

4.2.ReasonsforLiterals

Untilnow,weusedtheterm“reason”inanintuitiveway.Wewillnowdefinemoreformallywhatsuchrea-sonsareandhowtheycanbehandled.

Westartbyreviewingtheintuitionofreasonofaliteral(representingatruthvalueoftheliteral’satom).Arulea:-b,c,notd.cangiverisetothefollowingpropagation:Ifbandcaretrueanddisfalseinthecurrentpartialinterpretation,thenaisderivedtobetrue(byForwardPropagation).Inthiscase,wesaythataistrue“because”bandcaretrueanddisfalse.

Moregenerally,thereasonofaderivedliteralcon-sistsofthereasonsofthoseliteralsthatentailitstruth.WhileforForwardPropagationitisratherclearwhichliteralsentailthederivedone,thisissomewhatmoreintricateforotherpropagations.However,thereisonewayforaliteraltobecometrueunconditionally,i.e.nootherliteralsentailitstruth:Thesearethechosenliter-alswhichbecometruebyvirtueofoneoftherecursiveinvocationinthelasttwolinesofMGinFigure3.Inthiscase,theironlyreasonistheirchoice.

Theonlyelementaryreasonsarethereforethecho-senliterals;allotherreasonsareaggregationsofrea-sonsofotherliterals.Therearealsocasesinwhichlit-eralsareunconditionallytrue,forexampleatomsoc-curringinfacts(ruleswithsingletonheadandemptybody).Sinceatanypointduringthecomputationthereisauniquechosenliteralatanyrecursionlevel,wemayidentifythereasonofachosenliteralbyanin-

8F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

tegernumber(startingfrom0)representingitsrecur-sionlevel.Reasonsofderivedliteralsarethen(possi-blyempty)collectionsofintegers.

Eachliterallderivedduringthepropagation(throughDetCons)willhaveanassociatedsetofpositiveinte-gersR(l)representingthereasonofl,whichrepresentthesetofchoicesentailingl.Therefore,foranychosenliteralc,|R(c)|=1holds,whileforanyderived(i.e.,non-chosen)literaln,|R(n)|≥1holds.Forinstance,ifR(l)={1,3,4},thentheliteralschosenatrecursionlevels1,3and4entaill.

4.3.DeterminingReasonsforDerivedLiteralsInordertodefinemoreformallywhatreasonsforderived(non-chosen)literalsare—thistaskisoftenreferredtoasreasoncalculus—weneedsomepre-liminarynotions.

Givenaruler,a”satisfyingliteral”iseitheratrueheadatomorafalsebodyliteralinr.Rulerissatisfiediffithasasatisfyingliteral.Notethatasatisfiedrulecanhavemorethanonesatisfyingliterals.Alsonotethatanysatisfyingliteraliseitherachosenoraderivedliteral,sowemayassumethatitsreasonisknown.Letusnextdefineanordering≺ramongsatisfyingliteralsofagivenruler,whichisbasicallyalexico-graphicorderoverthenumericallyorderedintegersoftherespectivereasons.Wefirstgivetwotechnicaldef-initions:Rk(l)denotesthereasonoflwithoutthekgreatestintegers,whileMAXk(l)givesthek-thinte-gerofR(l)indescendingorder(or−1if|R(l)|R(l)=

󰀁

R(l),k=0

kRk−1(l)\\{max(RMAXk(l)=

󰀁

k−1(l))},k>0max(Rk−1(l)),Rk−1(l)=∅

−1,otherwise.wheremax(x)isthemaximumelementinthesetx.

Ifs1,s2aresatisfyingliteralsforruler,thens1≺s2(s1precedess2)iffonethefollowingconditionsholds:(i)MAX1(s1)(ii)MAX1(s1)=−1∧MAX1(s2)>0

(iii)∃k:k>1:∀x:1MAXk(s1)(iv)∃k:k>1:∀x:1MAXk(s1)=−1∧MAXk(s2)>0

Lets1∼s2ifs1≺s2ands2≺s1.Wewrites1󰀗s2iffs1≺s2ors1∼s2.

Lets1,...,snbesatisfyingliteralsforruler,ifsi󰀗sjforeachj=1,...,nthenRr=R(si)isacan-cellingassignmentforr.Notethatacancellingassign-mentofarulerrepresentsthereasoncorrespondingtotheearliestchoicecausingrtobesatisfied.

Inthefollowing,wedescribehowreasonsofderivedliteralsarecomputedfortherespectiveinferencerulesofDetConswithrespecttoapartialinterpretationI.Wewouldliketopointoutthatwedidnotintroduceanynovelinferencerulesinthiswork,butratherweextendexistingonesbythereasoncalculus.ForwardInference

Wehavealreadydiscussedthatcaseinformally;ifallbodyliteralsaretrue,allheadatomsbutone(whichisundefined)arefalse,thenweinferthetruthoftheonlyundefinedheadatom.Thereasonforthisheadatomisthesetconsistingoftheunionofthereasonsforalltheotherliteralsintherule.

Moreformally,givenaruler,if∃ai∈H(r)suchthat(i)∀b∈B(r):b∈I,(ii)∀a∈(H(r)\\{ai}):not󰀂a∈I,theninferaia∈H(example,r)\\{ai}R(nota)∪

Forconsiderthe󰀂

∈I.WedefineR(ai)aslfollowing∈B(r)R(l).program:

r1:avb:-c,notd.r2:c:-notd,e.r3:fvb.r4:gvd.r5:evh.

SupposeI={notb,c,notd,f,g,noth},andR(f)=R(notb)={1},R(c)={2,3},R(g)=R(notd)={2},andR(e)=R(noth)={3}.Wehavethataisderivedtobetruefromruler1(allbodyliteralsaretrueandtheonlyheadatombisfalse)andthereasonofatobetrueissettoR(a)=R(notb)∪R(c)∪R(notd)={1,2,3}.Kripke-KleeneNegation

Inthiscasewederivenegativeinformation:Ifforsomeundefinedatomalloftherules,inwhichitoccursinthehead,aresatisfiedw.r.t.I,thenderivethisatomtobefalse.Sothereasonforthederivedliteralisthatalloftherules,inwhichitoccursinthehead,aresatisfiedw.r.t.I.Asmotivatedabove,thereasonforarulebeingsatisfiedisitscancellingassignment.Thereasonoftheliteralishencetheunionoftherespectivecancellingassignments.

Givenanatoma,ifforeachrulersuchthata∈H(r)(i)∃b∈B(r)suchthatnot.b∈Ior(ii)∃c∈H(r)suchthata=cand󰀂c∈I,theninfernot.a∈I.WedefineR(a)asassignmentofruler:a∈rH.

(r)Rr,whereRrisacancellingForexample,considerthefollowingsubprogram:

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming9

r1:avb:-c,notd.r2:b:-e,notf.

r3:b:-g,h.

SupposeI={a,c,d,e,f,g,noth}andR(a)={7},R(c)={5},R(d)={6},R(e)={3},R(f)={4},R(g)={1},R(noth)={2}.Theatombisunde-finedanditiscontainedintheheadofallrules.Thecancellingassignmentsareasfollows:Rr1=R(c)={5},Rr2=R(e)={3},andRr3=R(g)={1}.DetConstheninfersbtobefalseandR(notb)=Rr1∪Rr2∪Rr3={1,3,5}.

ContrapositionforTrueHeads

Hereweexploitthefactthateachtrueatominasta-blemodelmusthaveatleastonesupportingrule.Ifanatomistrueandhasonlyonesupportingruleleft,weinferthetruthofallbodyliteralsandthefalsityofallotherheadatomsofthatrule.Notethatruleswhichdonotsupportthisatomaresatisfied,sotheyhaveacan-cellingassignment.Thereasonforallliteralsderivedinthiswayconsistofthefactthataistrueandthatallotherpossiblysupportingrulesaresatisfied,hencethereasonfortheatomunifiedwithallcancellingassign-mentsoftheotherrule.

Givenanatoma∈Iandarulersuchthata∈H(r),ifforeachruler′=rsuchthata∈H(r′)(i)∃b′∈B(r′):not.b′∈Ior(ii)∃c′∈H(r′):c′=a∧c′∈I,thenforeachc∈H(r)s.t.c=aandnotc∈Iinfernotc∈I,andforeachb∈B(r)\\Iinferb󰀂∈I.Foreachderivedliterallofr,R(l)=R(a)∪r′:a∈Hconsidering(r′)∧r′=rRr′.

Forexample,thefollowingprogram

r1:avb:-c,notd.r2:avg:-f.

r3:a:-k.

supposethatI={a,f,g,notk}andR(a)={2},R(f)={2},R(g)={3},R(notk)={1}.Theonlyunsatisfiedrulehavingaintheheadisr1andthecancellingassignmentsareRr2=R(a)=R(f)={2}andRr3=R(notk)={1}.InthiscaseweinfercandnotdandnotbandsetR(notb)=R(c)=R(notd)=R(a)∪Rr2∪Rr3={1,2}.ContrapositionforFalseHeads

Inordertoenforcesatisfactionofarule,iftheheadofaruleisfalse,andallbutone(undefined)bodyliteralsaretrue,weinferthattheremainingundefinedliteralmustbefalse.Inthiscase,thereasonforthefalsityofthatatomis–similartothecaseofForwardPropaga-tion–theunionofthereasonsforheadatomstobefalseandtheotherbodyliteralstobetrue.

Givenarulersuchthat(i)∀a∈H(r):not.a∈I,(ii)∃l∈B(r):l∈I∧not.l∈I,(iii)∀b∈B(r)\\

{󰀂

l}:b∈I,theninfer(r)R(nota)∪

Considerthefollowing󰀂not.l∈I.WesetR(l)=a∈Hb∈Bprogram,

(r)\\{l}R(b).r1:avb.:-c,d.r2:dvavb.r3:eva.r2::-d,b.

andsupposethatI={nota,notb,d,e},andR(nota)={1},R(notb)=R(d)={3},R(e)={2}.Byr1,wegetnotcandR(notc)=R(nota)∪R(notb)∪R(d)={1,3}.Well-foundedNegation

Inthiscaseweusetheresultthatanystablemodeldoesnotcontainanyatomwhichisinsomeunfoundedset(w.r.t.thestablemodel).Ifwedeterminethatsomesetofatomsisunfoundedw.r.t.thecurrentinterpretation,alloftheatomsinthissetcanbederivedasfalse.Thereasonforsomeatomtobeinanunfoundedsetisthatalloftherules,intheheadofwhichitoccurs,areei-thersatisfiedorcontainsomeatomoftheunfoundedsetinitspositivebody.Intheformercasethereasonisobviouslythecancellingassignment,whileinthelat-tercase,thereisnoreasonotherthanthepresenceoftheunfoundedsetitself.Sowheneverthereisareasonforthesatisfiedrulestobesatisfied,thisunfoundedsetwillexist.Thereforeunsatisfiedruleswithunfoundedpositivebodydonotcontributetothereason.

LetSbeanHCFsubprogramofP,Ibeanunfounded-freeinterpretation,andXbethegreatestunfoundedsetofSw.r.t.I.TheninferallatomsinXtobefalse.Foreachatoma∈thehead,setR(a)=R󰀂Xandforeachrulerwithainr∈S:a∈H(r)R∗

r,whereR∗risthecancellingassignmentofr,ifrissatisfied

w.r.t.I,or∗

r=∅ifrisnotsatisfiedw.r.t.I(inthelattercasercontainssomeotherelementfromX).Forexample,considerthefollowingprogram:

r1:avb.r2:a:-notc.r3:a:-d.r4:d:-a.r5:bve.r6:cvf.

SupposeI={b,c,note,notf},R(b)=R(note)={1},R(c)=R(notf)={2}.ThegreatestunfoundedsetisX={a,d},theninferaanddtobefalseandset

R(nota)=R(notd)=R∗

∪R∗{1,2},whereR∗

r1

r2∪R∗r∗r3∪R∗r4=1=R(b)={1},Rr2=R(c)={2}

andR∗

r3=R∗r4=∅.4.4.ReasonsforInconsistencies

Sofar,wehavedescribedwhatreasonsforliterals

areandhowtodeterminethem.Wewillnowturntohowtoexploitthemduringthecomputation.Asmo-tivatedbefore,wewillusereasoninformationwhen

10F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

inconsistenciesoccur,inordertounderstandwhatas-sumptionshavetobechangedinordertoavoidthein-consistency,andwhatotherassumptionsdonothaveanyinfluenceontheinconsistency.

InDLV,wecanisolatetwomainsourcesofincon-sistency:

1.Derivingconflictingliterals,and2.failingstabilitychecks.

Ofthesetwo,thesecondoneisparticularforSDLP,whilethefirstoneistheonlysourceforinconsistenciesinSATandnon-disjunctiveSLP.

Derivingconflictingliteralsmeans,inoursetting,thatDetConsdeterminesthatanatomaanditsnega-tionnotashouldbothhold.Inthiscase,therea-sonoftheinconsistencyis–ratherstraightforward–thecombinationofthereasonsforaandnota:R(a)∪R(not.a).Obviously,thisinconsistencyreasondoesnotdependontheinferencerulesusedwhende-terminingtheinconsistency.

ReconsideringtheexampleinSection4.1,therea-sonofthefirstinconsistencyistheunionofthereasonsforg,R(g)={0,2},andnotg,R(notg)={0,2},whichistheset{0,2}.Soonlytheliteralschosenatlevels0and2givereasontotheinconsistency,whiletheliteralchosenatlevel1(c)isdetachedfromtheinconsistency.

AsmentionedaboveinconsistenciesfromfailingstabilitychecksareapeculiarityofSDLP.Thissitua-tionoccursifthefunctionIsUnfoundedFree(I)ofFig-ure3returnsfalse.Intuitively,thismeansthatthecur-rentinterpretation(whichisguaranteedtobeamodel)isnotstable.From[21]weknowthatthisinterpreta-tionisnotunfounded-free,i.e.somepositivelyinter-pretedatomisinanunfoundedsetw.r.t.thisinterpre-tation.

Thissituationissimilartothewell-foundednega-tionoperatordescribedabove.Thedifferenceisthatincaseofafailedstabilitycheck,someunfoundedatomsarealreadytrueintheinterpretation,whiletheyarenormallyundefinedinthecaseofwell-foundednega-tion.NotethatwiththedefaultcomputationstrategyemployedinDLV,failedstabilitycheckswillbeduetosomenon-HCFsubprogram,asotherwisethewell-foundednegationoperatorwouldhavetriggeredbe-fore.

Thereasonforsuchaninconsistencyisthereforebasedonanunfoundedset,whichhasbeendeterminedduringIsUnfoundedFree(I).Givensuchanunfoundedset,thereasonfortheinconsistencyiscomposedofthecancellingassignmentsforsatisfiedruleswhich

containunfoundedatomsintheirhead.Aswithwell-foundednegation,unsatisfiedruleswithunfoundedatomsintheirheaddonotcontributetothereason.LetSbeanon-HCFsubprogramofP,Ibeanin-terpretation,andXbeanunfoundedsetofSw.r.t.I,suchthatI∩X=∅terminedasfollows:isthecancellingassignment=∅ifris󰀂.Theinconsistencyreasonisde-r∈S:a∈ofX∧∗,whereR∗

ra,∈ifHr(ris)Rsatisfiedr

w.r.t.

rI,orR∗

rnotsatisfiedw.r.t.I(inthelattercasercontainssomeotherelementfromX).4.5.UsingInconsistencyReasonsforBackjumpingWheninsideMG(cf.Figure3)someinconsistencyisdetected(inDetConsorIsUnfoundedFree),wean-alyzetheinconsistencyreason,andcangodirectlytothegreatestlevelintheinconsistencyreason.Goingtoanylevelinbetween(ifitexists)wouldindeedtrig-gertheencounteredinconsistencyagainandagain.Itisworthnoticingthatwhenaninconsistencyisencoun-teredduringDetCons,theinconsistencyreasonwillal-wayscontainthelastbutonelevel,amountingtosim-plebacktracking.

Theinconsistencyreasonscanbefurtherexploited:WheneverarecursiveinvocationofMGreturnsfalse,weknowthattherehasbeenaninconsistencyinthisbranch,andwecanre-usetheinconsistencyreasonsdeterminedinitfortheinconsistencyreasonofthere-spectivebranch,bystrippingoffallrecursionlevelswhicharegreaterthanthecurrentone.Thisisseman-ticallycorrect,asinthepresenceoftheremainingrea-sons,aninconsistencywilldefinitelyoccur.Ifatanylevel,bothrecursiveinvocationreturnfalse,weknowthattheentiresubtreeisinconsistent.Thereasonforthistreetobeinconsistentarethentheunionofthetwoinconsistencyreasonsofthebranches,minusthecur-rentlevel(astheinconsistencydoesnotdependonthechoiceofthecurrentlevel).Wecanthencontinuebygoingdirectlytothegreatestlevelinthisinconsistencyreason.

Thecasewherethesetechniquesallowforgoingdi-rectlytoalevel,whichisnotthepreviousrecursionlevel,isfrequentlyreferredtoasbackjumping,incon-trasttobacktracking.

4.6.ModelGeneratorwithBackjumping

InthissectionwedescribeMGBJ(showninFig.5),amodificationoftheMGfunction(asdescribedinsec-tion3),whichisabletoperformnon-chronologicalbacktracking,asdescribedinSection4.5.

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming11

ItextendsMGbyintroducingadditionalparametersanddatastructures,inordertokeeptrackofreasonsandtocontrolbacktrackingandbackjumping.Inpar-ticular,twonewparametersIRandbj

levelisalsousedtohold

thecurrentlevel.

Thevariablescurr

level){

bj

level=bj

level=MAX(IR);returnfalse;ReasonposIR,negIR;

SelectanundefinedatomAusingaheuristic;R(A)={curr

level)

returntrue;if(bj

level)

IR=posIR;returnfalse;

bj

level;R(notA)={curr

level)

returntrue;if(bj

level)

IR=negIR;returnfalse;

IR=trim(curr

level=MAX(IR);returnfalse;};

Fig.5.Computationofstablemodelswithbackjumping

Initially,theMGBJfunctionisinvokedwithIsettotheemptyinterpretation,IRsettotheemptyreason,andbj

leveltothemaximal

leveloftheinconsistencyreason(or0ifitistheemptyset)beforereturningfromthisinstanceofMGBJ.Ifthestabilitychecksucceeded,wejustreturntrue.

Otherwise,anatomAisselectedaccordingtoaheuristiccriterion.WesetthereasonofAtobethecur-rentrecursionlevelandinvokeMGrecursively,usingposIRandbj

leveltherecursionleveltobacktrackor

backjumpto.Now,ifbj

level

(whichisreinitializedbefore).

Asbefore,iftherecursivecallreturnstrue,MGBJimmediatelyreturnstruealso,whileifitreturnedfalse,wecheckwhetherwebackjump,settingIRandimme-diatelyreturningfalse.Ifnobackjumpisdone,thisin-stanceofMGBJistherootofaninconsistentsubtree,andwesetitsinconsistencyreasonIRtotheunion

12F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

ofposIRandnegIR,deletingallintegerswhicharegreaterorequalthanthecurrentrecursionlevel(thisisdonebythefunctiontrim),asdescribedinSection4.5.Wefinallysetbj

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming13

(shippedwiththesystem).Wehaveallowedatmostonehourofexecutiontimeforeachinstance.Forthosetests,wheretherearemultipleinstancesperinstancesize,theexperimentationwasstopped(foreachsys-tem)atthesizeatwhichsomeinstanceexceededthistimelimit.

5.2.BenchmarkProblems

BooleanSatisfiability.3SATisoneofthebestre-searchedproblemsinAIandgenerallyusedforsolv-ingmanyotherproblemsbytranslatingthemto3SAT,solvingthe3SATproblem,andtransformingthesolu-tionbacktotheoriginaldomain:

LetΦbeapropositionalformulainconjunctivemalform(CNF)Φ=󰀃n

nor-i=1(di,1∨...∨di,3)wherethedi,jareclassicalliteralsoverthepropositionalvari-ablesx1,...,xm.Φissatisfiable,iffthereexistsacon-sistentconjunctionIofliteralssuchthatI|=Φ.

3SATisaclassicalNP-completeproblemandcanbeeasilyrepresentedinSDLPasfollows:Foreachpropo-sitionalvariablexi(1≤i≤m),weaddthefollow-ingrulewhichensuresthatweeitherassumethatvari-ablexioritscomplementnxitrue:xivnxi.Foreachclaused1∨...∨d3inΦweaddthe:-notd¯1,...,notd¯3.

whered¯constraint

i(1≤i≤3)isxjifdiisapositiveliteralxj,andnxjifdiisanegativeliteral¬xj.

Ourtestinthisdomainincludesomerandomlygen-erated3SATproblemsand“structured”instances(cir-cuitverificationbenchmarks)fromthetheSuperscalarSuiteSSS.1.0ofMiroslavVelev,cf.[34].

Wehaverandomlygenerated203SATinstancesforeachproblemsizebyusingatoolbySelmanandKautz,whichisavailableatftp://ftp.research.att.com/dist/ai/.Thenumberofclausesforeachgeneratedinstanceis4.3timesthenumberofpropositionalvariables(inordertogeneratehardin-stances).TheSSS.1.0instances,availableinDIMACSformatwereeasilyconvertedinanequivalentSDLPprogramasindicatedabove.

Allinputfilesusedforthebenchmarksonrandominstancesareavailableonthewebathttp://www.mat.unical.it/leone/backjumping/aicom.tar.gz,whiletheSSS.1.0instancescanbefoundathttp://www.ece.cmu.edu/∼mvelev.

QuantifiedBooleanFormulas.ToassestheimpactofbackjumpingonΣP2-completeproblemsweused“∃∀”QuantifiedBooleanFormulas(2QBF)7,whichhaveal-readybeenusedinthepastforbenchmarkingSDLPsystems[9,12].

Theproblemhereistodecidewhetheraquanti-fiedBooleanformula(QBF)Φ=∃X∀Yφ,whereXandYaredisjointsetsofpropositionalvariablesandφ=C1∨...∨Ckisa3DNFformulaoverX∪Y,isvalid.Thetransformationfrom2QBFtodisjunctivelogicprogrammingweuseherehasbeengivenin[9],basedonareductionpresentedin[36].Theproposi-tionaldisjunctivelogicprogramPφproducedbythetransformationcontainsthefollowingrules:t(true).f(false).

t(X)vf(X):-exists(X).t(Y)vf(Y):-forall(Y).

w:-term(X,Y,Z,Na,Nb,Nc),

t(X),t(Y),t(Z),f(Na),f(Nb),f(Nc).

t(Y):-w,forall(Y).f(Y):-w,forall(Y).

:-notw.Moreover,Pφcontainsthefollowingfacts:–exists(v),foreachexistentialvariablev∈X;–forall(v),foreachuniversalvariablev∈Y;and–term(p1,p2,p3,q1,q2,q3),foreachdisjunctl1∧l2∧l3inφ,where(i)ifliisapositiveatomvi,thenpi=vi,otherwisepi=“true”,and(ii)ifliisanegatedatom¬vi,thenqi=vi,otherwiseqi=“false”.

Forexample,term(x1,true,y4,false,y2,false),encodesthetermx1∧¬y2∧y4.

The2QBFformulaΦisvalidiffPΦhasananswerset[36].

Weusedthebenchmarkinstancesfrom[9].There,50hardinstancesperproblemsizewererandomlygen-erated.Accordinglywith[37,38],eachformulacon-tainsthesamenumberofuniversalandexistentialvariables(|X|=|Y|),andthenumberofclausesisequaltothenumberofvariables(|X|+|Y|).Theinputfilesusedforthebenchmarksareavailableonthewebathttp://www.dlvsystem.com/examples/tocl-dlv.zip.

14F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

5.3.ExperimentalResults

Inthissectionwereporttheobtainedresults.Wewillfirstreportonthecasewithoutlookahead(i.e.usingtheweakheuristic),followedbytheresultswithlookahead(i.e.usingthestrongheuristic).

5.3.1.ResultswithoutLookahead

Westartreportingontherandom3SATinstances.Acriticalinternalmeasureisthenumberofchoicepoints,thesechoicepointscorrespondtothenumberoftimesMGorMGBJhavebeeninvoked.Ifback-jumpingoccurs,therewillbefewerchoicepoints.Onecouldalsocountthenumberofbackjumps,butthismeasurewouldbebogus,asobviouslynotonlythenumber,butalsothelengthofthebackjumpsareim-portant.Thenumberofchoicepoints,however,isadi-rectmeasureofthestructuralsavingsbroughtaboutbybackjumps.Fig.6showstheaverage(left)andmaxi-mum(right)numberofchoicepointsperinstancesize.Notethatwehaveemployedalogarithmicscaleinallofourdiagrams,astheymeasureconceptswhichgrowexponentially.BJNscalesslightlybetter,inthefi-nalinstancesize(155),BJNtakesabout800000fewerchoicepointsthanSTDNonaverage,whilethemax-imumnumberofchoicepointsconsumedforthisin-stancesizeisalmost4millionmoreforSTDN.

Buthavingbackjumpingalsoincurssomeoverhead(mostimportantly,maintainingreasons),whichcanobviouslynotbemeasuredintermsofchoicepoints.SoinFig.7,wereportontheaverage(left)andmax-imum(right)executiontime.Weobservethatthepo-tentialbenefitsofsavedchoicepointsisoutweighedbytheoverheadincurredbythereasoncomputations,butimportantly,thereisnoslowdown.

Letusnowturntothestructuredsatisfiabilityin-stances.Here,wehaveallowedtwohoursofexecutiontime,andreportonlyonthoseinstances,whichhavebeensolvedbyatleastoneofthetestedsystemsintheallottedtime.TheexecutiontimesarereportedinTa-ble1,andchoicepointsarereportedinTable2.WecanseethatSTDNwasnotabletosolveanyoftheseinstanceswithin2hours.BJN,however,couldsolveoneinstance(dlx1

BJNSTDLdlx1

5464.80s

306.33s

dlx2

bug04>2h

2.91s

cc>2h

>2h

dlx2

bug07

>2h

814.97s

cc>2h

1890.81s

BJN

STDLdlx179989185

221925

dlx2

bug04

-154

cc--dlx2

bug07

-88965

cc-295785

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming15

10000000100000000BJNSTDNAverage Number of ChoicepointsMaximum Number of Choicepoints1000000100000100001000100101100000001000000100000100001000100101BJNSTDNNumber of Propositional variables

Number of Propositional variablesFig.6.ChoicepointsonRandom3SATinstanceswithoutlookahead

1000BJNSTDN10000BJNSTDNAverage Time (s)100Maximum Time (s)Number of Propositional variables10001001010110,10,10,010,01Number of Propositional variablesFig.7.ExecutionTimesonRandom3SATproblemswithoutlookahead

Average Number of ChoicepointsBJNSTDN10000Maximum Number of Choicepoints100000100000001000000BJNSTDN10000010001000010010001001010148121620242832364044485256606468727680148121620242832364044485256606468727680Number of Propositional variablesNumber of Propositional variables

Fig.8.Choicepointsonrandom2QBFproblemswithoutlookahead

backjumpingdoesbasicallynothaveanyimpacthere(weomitthisgraph,asitshowsjusttwooverlappinglines).However,lookingatFig.10,where,asusual,theaveragetimeisreportedintheleftgraph,andthemaximumtimeintherightone,weobservethattheoverheadinexecutiontimeisverysmall.

LookingattheresultsofthestructuredSATin-stancesinTables1and2,thepictureisquitedifferent:AlreadySTDLcansolvemanymoreinstancesthanSTDNwithin2hours,butBJLmanagestosolveone(dlx2bug06)within2hours,whichnoothertestedsystemcoulddo.Alsointheotherexamples,BJLisalwaysthefastestsystem,sometimesmorethantwiceasfastasSTDL.Alsothenumberofchoicepointsis

16F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

10010000BJNSTDNBJNSTDNAverage Execution Time (s)10Maximum Execution Time (s)1000100148121620242832364044485256606468727680101481216202428323640444852566064687276800,10,10,010,01Number of Propositional variablesNumber of Propositional variables

Fig.9.Executiontimeonrandom2QBFproblemswithoutlookahead

1000BJLSTDL10000BJLSTDLAverage Time (s)100Maximum Time (s)Number of Propositional variables10001001010110,10,10,010,01Number of Propositional variablesFig.10.Executiontimeonrandom3SATproblemswithlookahead

alwaysdrasticallylowerforBJLthanforSTDL.

Finally,wereportontheexperimentswith2QBFinstances.Fig.11showstheaverage(left)andmaxi-mum(right)numberofchoicepointsperinstancesize.Weseethatalsowithlookahead,thenumberofchoicepointsiscuteffectivelybyBJLwithrespecttoSTDL.Fig.11reportstheaverage(left)andmaximum(right)executiontimeperinstancesize.Alsohere,BJLclearlyhasanedgeoverSTDL.BJLalsomanagedtosolvemoreinstanceswithintheallottedtimethanSTDL.5.3.3.Summary

Wehaveobservedthatbothwithandwithoutlooka-head,backjumpinggenerallycutsthesearchspaceef-fectivelyandconsumes(oftendramatically)lessex-ecutiontimethanthesystemswithoutbackjumping.Theonlyexceptionis3SATonrandominstances,whereBJLhasamildoverheadinexecutiontime.ButthisminimaloverheadisdefinitelyoutweighedbythebigadvantagesBJLandBJNshowonstructuredSATand2QBFinstances,bothwithandwithoutheuristics.Aconsequenceoftheseresultsisthatbackjumpingwithoutclauselearningis,atleastforSDLP,effective.

6.ConclusionandFutureWork

Wehavepresentedabackjumpingtechniqueforcomputingthestablemodelsofdisjunctivelogicpro-grams.Itisbasedonareasoncalculusandisanelabo-rationoftheworkin[1,2],butourworkcontainssomecrucialnoveltiesandimprovements:Mostimportantly,ourframeworkissuitableandtailoredfordisjunctiveprograms,includingnoveltechniquesforthissetting.Concerningthereasoncomputation,ourmethoddoesnotincurbuildinganimplicationgraph,butratherstoreonlysetsofintegers,whicharemoreefficienttocom-pute,andalsogiveaneasierhandleondeterminingthepointtojumpto.

WehaveimplementedthetechniqueintheDLVsys-tem,andhaveconductedseveralexperimentswithit.Intotal,thebackjumpingtechniquehasaverypos-itiveeffectonperformanceinmanycases,andevenincases,inwhichitcannotcutthesearchspace,itsoverheadisnegligible.Moreover,theseimprovementscanbeobservedwitheitheroftwoheuristicmethods,whicharediametricallydifferentfromeachother.SoweconcludethatthetechniqueforSDLPisrobustwith

F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming17

Average Number of ChoicepointsMaximum Number of Choicepoints10000010000000BJLSTDL10000BJLSTDL10000001000001000100001000100100101014812162024283236404448521481216202428323640444852Number of Propositional variablesNumber of Propositional variables

Fig.11.ChoicePointsonrandom2QBFproblemswithlookahead

10010000BJLSTDLBJLSTDL10Maximum Execution Time (s)Average Execution Time (s)100010014812162024283236404448521014812162024283236404448520,10,10,010,01Number of Propositional variablesNumber of Propositional variables

Fig.12.Executiontimeonrandom2QBFproblemswithlookahead

respecttotheheuristicmethod,andinparticular,co-operateswellwithalookaheadheuristic.

Ourbackjumpingtechniqueisveryeffectiveonstructuredsatisfiabilityinstances,andonrandomlygeneratedhard2QBFinstances(whichcannotbesolvedbySATsolversdirectlyunderstandardcom-plexityassumptions).Itshowslittletonoimpact,butalsonorelevantslowdownonrandomlygeneratedhardsatisfiabilityinstances.

Forfuturework,wewanttoaddresstheques-tionwhetherclauselearningcanyieldanadditionalgainw.r.t.backjumpinginSDLP.ImplementingclauselearninginDLVis,however,notstraightforwardatall,astheDLVmodelgeneratorheavilyreliesontheas-sumptionthattheprogram,onwhichitworks,isfixed.Thereareseveralwaysofovercomingthisdifficulty,rangingfromaredesignofthedatastructurestothein-troductionofanadditionalstructurewhichisdedicatedtothelearnedclauses.

Anotherpossibilityforfutureworkistostudytheuseofourreasoncalculusnotonlyforstablemodelcomputation,butalsoforsoftwareengineeringtasks.Inparticular,ithasbeenobservedthatreasonscouldbe

profitablyusedfordebuggingSDLPprograms.Apro-gram,forwhichsomeparticularstablemodel,whichhasbeenexpectedbyitsauthor,doesnotexist,thesereasonscouldbeusedtofindthepointinthepro-gramwhichforbidstheexistenceoftheexpectedstablemodel,andthusthemodelingbug.Acknowledgements

ThisworkwassupportedbytheEuropeanCommis-sionunderprojectsIST-2002-33570INFOMIXandIST-2001-37004WASP,andwaspartiallysupportedbyM.I.U.R.underproject”Sistemibasatisullalogicaperlarappresentazionediconoscenza:estensionietec-nichediottimizzazione”.WolfgangFaber’sworkwasfundedbyanAPARTgrantoftheAustrianAcademyofSciences.References

[1]Ward,J.,Schlipf,J.S.:AnswerSetProgrammingwithClause

Learning.In:LPNMR-7.LNCS,(2004)302–313

18F.Riccaetal./ABackjumpingTechniqueforDisjunctiveLogicProgramming

[2]Ward,J.:AnswerSetProgrammingwithClauseLearning.PhDthesis,OhioStateUniversity,Cincinnati,Ohio,USA(2004)[3]

Lifschitz,V.:AnswerSetPlanning.InSchreye,D.D.,ed.:ICLP’99,LasCruces,NewMexico,USA,TheMITPress(1999)23–37

[4]Eiter,T.,Gottlob,G.,Mannila,H.:DisjunctiveDatalog.ACMTODS22(1997)364–418

[5]

Rintanen,J.:ImprovementstotheEvaluationofQuanti-fiedBooleanFormulae.InDean,T.,ed.:IJCAI1999,Swe-den,(1999)1192–1197

[6]Eiter,T.,Gottlob,G.:TheComplexityofLogic-BasedAbduc-tion.JACM42(1995)3–42

[7]Baral,C.:KnowledgeRepresentation,ReasoningandDeclara-tiveProblemSolving.CUP(2002)

[8]

Leone,N.,Rosati,R.,Scarcello,F.:EnhancingAnswerSetPlanning.In:IJCAI-01WorkshoponPlanningunderUncer-taintyandIncompleteInformation.(2001)33–42

[9]

Leone,N.,Pfeifer,G.,Faber,W.,Eiter,T.,Gottlob,G.,Perri,S.,Scarcello,F.:TheDLVSystemforKnowledgeRepresentationandReasoning.ACMTOCL(2005)Toappear.[10]

Janhunen,T.,Niemel¨a,I.,Seipel,D.,Simons,P.,You,J.H.:Un-foldingPartialityandDisjunctionsinStableModelSemantics.Tech.Reportcs.AI/0303009,arXiv.org(2003)

[11]

Lierler,Y.:DisjunctiveAnswerSetProgrammingviaSatisfia-bility.In:LogicProgrammingandNonmonotonicReasoning—8thInternationalConference,LPNMR’05,Diamante,Italy,2005,Proceedings.LNCS3662

[12]

Koch,C.,Leone,N.,Pfeifer,G.:EnhancingDisjunctiveLogicProgrammingSystemsbySATCheckers.ArtificialIntelli-gence15(2003)177–212

[13]Prosser,P.:HybridAlgorithmsfortheConstraintSatisfactionProblem.ComputationalIntelligence9(1993)268–299

[14]

Dechter,R.,Frost,D.:Backjump-basedbacktrackingforcon-straintsatisfactionproblems.ArtificialIntelligence136(2002)147–188

[15]

Bayardo,R.,Schrag,R.:UsingCSPLook-backTechniquestoSolveReal-worldSATInstances.In:Proceedingsofthe15thNationalConferenceonArtificialIntelligence(AAAI-97).(1997)203–208

[16]

Moskewicz,M.W.,Madigan,C.F.,Zhao,Y.,Zhang,L.,Malik,S.:Chaff:EngineeringanEfficientSATSolver.In:Proceed-ingsofthe38thDesignAutomationConference,DAC2001,LasVegas,NV,USA,18-22,2001,ACM(2001)530–535[17]

Eiter,T.,Faber,W.,Leone,N.,Pfeifer,G.:DeclarativeProblem-SolvingUsingtheDLVSystem.InMinker,J.,ed.:Logic-BasedArtificialIntelligence.Kluwer(2000)79–103[18]Gelfond,M.,Lifschitz,V.:ClassicalNegationinLogicPro-gramsandDisjunctiveDatabases.NGC9(1991)365–385[19]Przymusinski,T.C.:StableSemanticsforDisjunctivePro-grams.NGC9(1991)401–424

[20]

Marek,W.,Subrahmanian,V.:TheRelationshipbetweenLogicProgramSemanticsandNon-MonotonicReasoning.In:ICLP’89,MITPress(1989)600–617

[21]

Leone,N.,Rullo,P.,Scarcello,F.:DisjunctiveStableModels:UnfoundedSets,FixpointSemanticsandComputation.Infor-mationandComputation135(1997)69–112

[22]

Baral,C.,Gelfond,M.:LogicProgrammingandKnowledgeRepresentation.JLP19/20(1994)73–148

[23]VanGelder,A.,Ross,K.,Schlipf,J.:TheWell-FoundedSe-manticsforGeneralLogicPrograms.JACM38(1991)620–650[24]Ben-Eliyahu,R.,Dechter,R.:PropositionalSemanticsforDis-junctiveLogicPrograms.AMAI12(1994)53–87[25]Faber,W.:EnhancingEfficiencyandExpressivenessinAnswer

SetProgrammingSystems.PhDthesis,TUWien(2002)[26]Niemel¨a,I.,Simons,P.:EfficientImplementationoftheWell-foundedandStableModelSemantics.InMaher,M.J.,ed.:

ICLP’96,Bonn,Germany,MITPress(1996)289–303[27]Simons,P.:ExtendingandImplementingtheStableModelSe-mantics.PhDthesis,HelsinkiUniversityofTechnology,Fin-land(2000)[28]Faber,W.,Leone,N.,Mateis,C.,Pfeifer,G.:UsingDatabase

OptimizationTechniquesforNonmonotonicReasoning.InDDLP’99,PrologAssociationofJapan(1999)135–139

[29]Faber,W.,Leone,N.,Pfeifer,G.:ExperimentingwithHeuris-ticsforAnswerSetProgramming.In:IJCAI2001,Seattle,WA,USA,(2001)635–640[30]Faber,W.,Leone,N.,Pfeifer,G.:OptimizingtheComputa-tionofHeuristicsforAnswerSetProgrammingSystems.In:LPNMR’01.LNCS2173[31]Faber,W.,Leone,N.,Pfeifer,G.:PushingGoalDerivationin

DLPComputations.In:LPNMR’99.LNCS1730

[32]Calimeri,F.,Faber,W.,Leone,N.,Pfeifer,G.:PruningOper-atorsforAnswerSetProgrammingSystems.In:NMR’2002.(2002)200–209[33]Lynce,I.,Silva,J.P.M.:Buildingstate-of-the-artsatsolvers.

InvanHarmelen,F.,ed.:Proceedingsofthe15thEureopeanConferenceonArtificialIntelligence(ECAI2002),IOSPress(2002)166–170[34]Velev,M.N.,Bryant,R.E.:SuperscalarProcessorVerifica-tionUsingEfficientReductionsoftheLogicofEqualitywithUninterpretedFunctionstoPropositionalLogic.In:CorrectHardwareDesignandVerificationMethods,10thIFIPWG10.5AdvancedResearchWorkingConference,CHARME’99,BadHerrenalb,Germany,27-29,1999,Proceedings.NY,USA,(1999)37–53

[35]Papadimitriou,C.H.:ComputationalComplexity.Addison-Wesley(1994)

[36]Eiter,T.,Gottlob,G.:OntheComputationalCostofDisjunc-tiveLogicProgramming:PropositionalCase.AMAI15(1995)289–323[37]Cadoli,M.,Giovanardi,A.,Schaerf,M.:ExperimentalAnal-ysisoftheComputationalCostofEvaluatingQuantifiedBooleanFormulae.In:AI*IA97.Italy,(1997)207–218

[38]Gent,I.,Walsh,T.:TheQSATPhaseTransition.In:AAAI.

(1999)