**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 = 2^{31}). 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(P_{R}, P_{K}, ∅, {⊥}, ∅), 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