Claire Lefevre and Pascal Nicolas, LERIA, University of Angers, France
| Abstract. ASPeRiX is an ASP solver implementing an innovative strategy for the computation of stable models [1] of a normal logic program. Its main specificity is to realize a forward chaining of first order rules that are grounded on the fly during the computation of the answer sets. So, unlike all others available ASP systems, ASPeRiX does not need a pregrounding processing.
The system is implemented in C++ and is available (under GPL) at http://www.info.univ-angers.fr/pub/claire/asperix. |
Language
ASPeRiX deals directly with any normal logic program containing rules like
where atoms can contain variables and function symbols.
Arithmetic calculus is also possible by means of numeric constants, variables, binary operators +, –, *, / and mod, unary operator abs and parenthesis. It can occur in an assignment expression (as Z=Y-(X mod 2)) or inside an atom (as r(g(X+Y))).
Comparison between two arithmetic expressions or two symbolic constants are allowed in the positive body of a rule with the operators ==, !=, <, <=, >, >=. Equality and inequality operators can also be used for functional terms. To avoid the possible problem of infinite Herbrand universe due to function symbols and arithmetic calculus, the user can pass to ASPeRiX the command line parameters -F k to limit to k the number of nestings in functional terms and -N k to limit the set of numbers to [–k,…,k] (maximum value: k = 231). Some additional directives, as #hide p/k. and #show p/k. are available to filter the output of predicates p with arity k.
The only syntactic restriction is the safety of rules. That is every variable that appears in a rule must occur also in a predicate atom or on the left side of an assignment atom of the positive body of the rule.
Algorithm
| Algorithm 1: Algorithm of ASPeRiX. Function Solve( PR,PK, IN, OUT, CR); repeat // propagation phase r0 ← γpro(PR ∪ PK,IN,OUT,CR); if r0 then IN ← IN ∪{head(r0)}; CR ← CR ∪{r0}; until ¬r0; if IN ∩ OUT ⁄= ∅ then // contradiction detected return false; else r0 ← γcho(PR, IN, OUT, CR); if ¬r0 then if γcho(PK, IN, OUT, ∅) then // constraint not satisfied return false; else // an answer set is found return IN; else//choice point stop ← solve(PR, PK, IN ∪{head(r0)}, OUT ∪ body–(r0), CR ∪{r0}); if ¬stop then stop ← solve(PR, PK ∪{⊥← body–(r0)}, IN, OUT, CR ∪{r0}); |
The search procedure of ASPeRiX for computing the answer set of a program P is
given in Algorithm 1 that must be called by solve(PR, PK, ∅, {⊥}, ∅), knowing
that 
(the constraint set) and 
. CR (for
chosen rules) is the set of rules grounded and applied during the search. The
procedure follows a forward chaining that alternates two steps: a monotonic
propagation phase that applies the largest possible number of monotonic rule
instances built by γpro function, and a choice point that applies an instance of one
non monotonic rule built by γcho function. At each time, γpro or γcho builds some
ground instances of rules by unifying atoms of the positive body with atoms occurring
in IN and propagating this unifier in the head and the negative body of
the rule. In order to limit the number of these unifications, ASPeRiX uses a
dependency graph between predicates to group them in maximal strongly
connected components that are themselves ordered. Propagation and choice
steps build incrementally two atom sets IN and OUT representing atoms
occurring or not in the solution. All along the search process, the condition
IN ∩ OUT = ∅ is checked and if it is violated a backtrack is done. In this
case, the last applied non monotonic rule is then retracted and its negative
body is added as a new constraint in order to record that this rule has to be
blocked.
Even if the algorithm describes the computation of one answer set (or no one if
the program is inconsistent) it has been extended in ASPeRiX to compute an arbitrary
number of (or all) answer sets of P.
References