Techniques for Efficient Lazy-Grounding ASP Solving LorenzLeutgeb1 AntoniusWeinzierl1,2 September19,2017 1Knowledge-BasedSystemsGroup TUWien,Vienna,Austria 2DepartmentofComputerScience AaltoUniversity,Helsinki,Finland Introduction Motivation • Answer-SetProgramming(ASP):well-establishedKRformalism. • Rule-based,nonmonotonic,expressive. • TraditionalASPsolvingtwo-phased: groundandsolve. • Problem: groundingofexponentialsizeingeneralandpractice. ⇒ GroundingbottleneckofASP. Example dom(1). dom(2). ... dom(20). sel(X) ← dom(X),notnsel(X). nsel(X) ← dom(X),notsel(X). ← sel(Y),sel(X),X! = Y. p(X ,X ,X ,X ,X ,X ) ← sel(X ),sel(X ),sel(X ), 1 2 3 4 5 6 1 2 3 sel(X ),sel(X ),sel(X ). 4 5 6 1 Motivation • Answer-SetProgramming(ASP):well-establishedKRformalism. • Rule-based,nonmonotonic,expressive. • TraditionalASPsolvingtwo-phased: groundandsolve. • Problem: groundingofexponentialsizeingeneralandpractice. ⇒ GroundingbottleneckofASP. Example dom(1). dom(2). ... dom(20). sel(X) ← dom(X),notnsel(X). nsel(X) ← dom(X),notsel(X). ← sel(Y),sel(X),X! = Y. p(X ,X ,X ,X ,X ,X ) ← sel(X ),sel(X ),sel(X ), 1 2 3 4 5 6 1 2 3 sel(X ),sel(X ),sel(X ). 4 5 6 1 Lazy-Grounding ASP Solving • Lazy-Grounding: interleavegroundingandsolving ⇒Avoidgroundingbottleneck. • Basedoncomputationsequences. • Existingsolvers: Gasp,AsPeRiX,Omiga. • Nostrongsearchspacereducingtechniques (likeconflict-drivenlearning,backjumping,heuristics,etc). • Groundingstrongly-coupledtosearch(grounderbacktracks). ⇒ Badsearchperformance. 2 The Alpha Solver • Novelapproachatlazy-grounding(firstpresentedatLPNMR’17). • Twocomponents: lazy-grounderandmodifiedCDNLsolver. • Blendlazy-groundingandstate-of-the-artCDNL-basedsearch. • Representrulesbynogoods(similartoClasp/Clingo). • Loose-couplingoflazy-groundingandsearch. • Goal: Lazy-groundingwithgoodsearchperfomance. 3 Overview of Alpha Architecture of Alpha Nogoods Grounder Solver Program Conflict Nogood Parser Resolution Storage Lazy- Choice Decision Assignment Grounding Atoms Heuristic Answer-Set partialAssignment Figure1: Alphaarchitecture,arrowsindicatedataflow. 4 Representing Rules • Constraint: ← sel(1),sel(2). • Nogood: ng = {Tsel(1),Tsel(2)}. • Problem: distinguish← nota,b.froma ← b. • State-of-the-artsolution,addconstraintexpressing: “Ifaistrue,theremustbearulefiringwithainitshead.” • Lazy-groundingcannotknowallruleswithainthehead: a ← p(X). • SolutioninAlpha: • Nogoodsmayhaveheadandthirdtruthvaluemust-be-true. • Propagate: totrueifheadofnogoodisimplied,otherwiseto must-be-true(andfalse). • Nogood{Fa,Tb}distinctfrom{Fa,Tb} withhead. 1 5 Representing Rules • Constraint: ← sel(1),sel(2). • Nogood: ng = {Tsel(1),Tsel(2)}. • Problem: distinguish← nota,b.froma ← b. • State-of-the-artsolution,addconstraintexpressing: “Ifaistrue,theremustbearulefiringwithainitshead.” • Lazy-groundingcannotknowallruleswithainthehead: a ← p(X). • SolutioninAlpha: • Nogoodsmayhaveheadandthirdtruthvaluemust-be-true. • Propagate: totrueifheadofnogoodisimplied,otherwiseto must-be-true(andfalse). • Nogood{Fa,Tb}distinctfrom{Fa,Tb} withhead. 1 5