Graph Theoretical Characterization and Computation of Answer Sets

1 Introduction

Answer set semantics [Gelfond and Lifschitz, 1991] was established as an alternative declarative semantics for logic programs. Originally, it was defined for extended logic programs 1 [Gelfond and Lifschitz, 1991] as a generalization of the stable model semantics [Gelfond and Lifschitz, 1988]. Currently there are various applications of answer set programming, e.g. [Dimopoulos et al., 1997; Liu et al., 1998; Niemel¨a, 1999]. Furthermore, there are reasonably efficient implementations available for computing answer sets, e.g. smodels [Niemel¨a and Simons, 1997] and dlv [Eiter et al., 1997]. Systems, like DeReS [Cholewi´nski et al., 1996] and quip [Egly et al., 2000], are also able to compute answer sets, although they were designed to deal with more general formalisms.

Both systems and most of the theoretical results as well deal with answer sets in terms of atoms (or literals). This paper aims at a different point of view, namely characterizing and computing answer sets in terms of rules. Intuitively, the head D4 of a rule D4 AW D5 BD BN BM BM BM BN D5 D2 BN D2D3D8 D7 BD BN BM BM BM BN D2D3D8 D7 CZ is in some answer set BT if D5 BD BN BM BM BM BN D5 D2 are in BT and none of D7 BD BN BM BM BM BN D7 CZ is in BT. Let

be a logic program and let us call the rules D6 CP , D6 CQ , D6 CR , D6 CS , D6 CT , and D6 CU , respectively. Then  has two different answer sets BT BD BP CUCSBN CQBN CRBN CPBN CUCV and BT BE BP CUCSBN CQBN CRBN CTCV. It is easy to see that the application of D6 CU blocks the application of D6 CT wrt BT BD , because if D6 CU contributes to BT BD , then CU BE BT BD and thus D6 CT cannot be applied. Analogously, D6 CT blocks D6 CP wrt answer set BT BE . This observation leads us to a strictly blockage-based approach. More precisely, we represent the block relation between rules as a so-called block graph. Answer sets then are characterized as special non-standard graph colorings of block graphs. Each node of the block graph (corresponding to some rule) is colored with one of two colors, representing application or non-application of the corresponding rule. The block graph has quadratic size of the corresponding logic program. Since the block graph serves as basic data structure for our implementation, it needs polynomial space.

1 Extended logic programs are logic programs with classical negation.

2 Background

We deal with normal logic programs which contain the symbol D2D3D8 used for negation as failure. A rule, D6, is any expression of the form

where D4, D5 CX (BCAKCXAKD2) and D7 CY (BCAKCYAKCZ) are atoms. A rule is a fact if D2BPCZBPBC, it is called basic if CZBPBC. For a rule D6 we define CWCTCPCSB4D6B5BPD4 and CQD3CSDDB4D6B5BPCUD5 BD BN BM BM BM BN D5 D2 BN D2D3D8 D7 BD BN BM BM BM BN D2D3D8 D7 CZ CV. Furthermore, let CQD3CSDD B7 B4D6B5BPCUD5 BD BN BM BM BM BN D5 D2 CV denote the positive part and CQD3CSDD A0 B4D6B5BPCUD7 BD BN BM BM BM BN D7 CZ CV the negative part of CQD3CSDDB4D6B5. Definitions of the head, the body, the positive and negative body of a rule are generalized to sets of rules in the usual way. The elements of CQD3CSDD B7 B4D6B5 are referred to as the prerequisites or positive body atoms of D6. The elements of CQD3CSDD A0 B4D6B5 are referred to as the negative body atoms of D6. If CQD3CSDD B7 B4D6B5BPBN, then D6 is said to be prerequisite-free. A set of rules of the form (2) is called a (normal) logic program. A program is called prerequisite-free if each of its rules is prerequisite-free. We denote the set of all facts of program  by BY  .

Let D6 be a rule. D6 B7 then denotes the rule CWCTCPCSB4D6B5 AW CQD3CSDD B7 B4D6B5. For a logic program let  B7 BPCUD6 B7 CY D6 BE CV. A set of atoms CG is closed under a basic program  iff for any D6BE , CWCTCPCSB4D6B5BECG whenever CQD3CSDDB4D6B5 AI CG. The smallest set of atoms which is closed under a basic program  is denoted by CnB4 B5.

The reduct,  CG , of a program relative to a set CG of atoms is defined by  CG BPCUD6 B7 CY D6BE and CQD3CSDD A0 B4D6B5 CK CG BP BNCVBM We say that a set CG of atoms is an answer set of a program iff CnB4 CG B5 BP CG. The reduct  CG is often called the GelfondLifschitz reduction. Observe, that there are programs, e.g. CUD4 AW D2D3D8 D4CV, that do not possess an answer set. Throughout this paper, we use the term "answer set" instead of "stable model" since it is the more general one.

A set of rules CB of the form (2) is grounded iff there exists an enumeration CWD6 CX CX CXBE
of CB such that for all CXBE
we have that CQD3CSDD B7 B4D6 CX B5 AI CWCTCPCSB4CUD6 BD BN BM BM BM BN D6 CXA0BD CVB5BM For a set of rules CB and a set of atoms CG we define the set of generating rules of CB wrt CG as follows

The following result relates groundedness and generating rules to answer sets.

Lemma 2.1 Let  be a logic program and CG be a set of atoms. Then CG is an answer set of  iff (i) BZCAB4BNCGB5 is grounded and (ii) CGBPCnB4BZCAB4BN CGB5 B7 B5.

This lemma characterizes answer sets in terms of generating rules. Observe, that in general BZCAB4BNCGB5 B7 BIBP  CG (take  BP CUCP AWBN CQ AW CRCV and CG BP CUCPCV).

Assume that for each program we have

In Section 5, we show how to generalize our approach to both normal logic programs with multiple positive body atoms and also to extended logic programs. Therefore, the assumption above is not a real restriction.

We need some graph theoretical terminology. A directed graph BZ is a pair BZ BP B4CEBNBTB5 such that CE is a finite, nonempty set (vertices) and BT AI CE A2CE is a set (arcs). For a directed graph BZ BP B4CEBNBTB5 and a vertex DA BE CE , we define the set of all predecessors of DA as AD A0 B4DAB5 BP CUD9 CY B4D9BN DAB5 BE BTCV. Analogously, the set of all successors of DA is defined as AD B7 B4DAB5BPCUD9 CY B4DABN D9B5BEBTCV. A path from DA to DA BC in BZBPB4CEBNBTB5 is a finite subset  DADA BC AI CE such that  DADA BC BP CUDA BD BN BM BM BM BN DA D2 CV, DABPDA BD , DA BC BPDA D2 and B4DA CX BN DA CXB7BD B5BEBT for each BDAKCXBOD2. The arcs of a path  DADA BC are defined as BTD6CRD7B4 DADA BC B5 BPCUB4DA CX BN DA CXB7BD B5 CY BDAK CXBOD2CV. A path from DA to DA for some DABECE is called a cycle in BZ.

In order to represent more information in a directed graph, we need a special kind of labeled graphs. B4CEBNBT BC CJ BT BD B5 is a directed graph whose arcs BT BC CJ BT BD are labeled with zero (0-arcs) and with one (1-arcs), respectively. For BZ we distinguish 0-predecessors (0-successors) from 1-predecessors (1successors) denoted by AD A0 BC B4DAB5 (AD B7 BC B4DAB5) and AD A0 BD B4DAB5 (AD B7 BD B4DAB5) for DA BE CE , respectively. A path  DADA BC in BZ is called 0-path if BTD6CRD7B4 DADA BC B5 AI BT BC . The length of a cycle in a graph B4CEBNBT BC CJ BT BD B5 is the total number of 1-arcs occurring in the cycle. Additionally, we call a cycle even (odd) if its length is even (odd).

3 Block Graphs and Application Colorings

We now go on with a formal definition of the conditions under which a rule blocks another rule.

Definition 3.1 Let  be a logic program s.t. condition (4) holds, and let  BC AI  maximal grounded. The block graph A0  BP B4CE  BN BT BC  CJBT BD  B5 of  is a directed graph with vertices CE  BP  and two different kinds of arcs defined as follows

Observe, that there exists a unique maximal grounded set  BC AI  for each program, that is, A0  is well-defined. This definition captures the conditions under which a rule D6 BC blocks another rule D6 (e.g. B4D6 BC BN D6B5 BE BT BD ). We also gather all groundedness information in A0  , due to the restriction to rules in the maximal grounded part of logic program  . This is important because a block relation between two rules D6 BC and D6 becomes effective only if D6 BC is groundable through other rules. E.g. for program  BP CUD4 AW D5BN D5 AW D4CV the maximal grounded subset of rules is empty and therefore A0  contains no 0-arcs. Figure 1 shows the block graph of program (1).

We now define so-called application colorings or acolorings for block graphs. A subset of rules BZ D6 AI  is a grounded 0-path for D6 BE  if BZ D6 is a 0-path from some fact to D6 in A0  .

Definition 3.2 Let  be a logic program s.t. condition (4) holds, let A0  BP B4BNBT BC  CJ BT BD  B5 be the corresponding block graph and let CR BM  BJAX CUA9BNA8CV be a mapping. Then CR is an a-coloring of A0  iff the following conditions hold for each D6 BE 

BTBD CRB4D6B5 BP A9 iff one of the following conditions holds a. AD A0 BC B4D6B5 BIBP BN and for each D6 BC BEAD A0 b. there is some D6 BCBC BEAD A0 BD B4D6B5 s.t. CRB4D6 BCBC B5 BP A8.

BC B4D6B5 we have CRB4D6 BC B5 BP A9 BTBE CRB4D6B5 BP A8 iff both of the following conditions hold a. AD A0 BC B4D6B5BPBN or it exists grounded 0-path BZ D6 s.t. CRB4BZ D6 B5BPA8 2 b. for each D6 BCBC BEAD A0 BD B4D6B5 we have CRB4D6 BCBC B5 BP A9.

Let CR be an a-coloring of some block graph A0  . Rules are then intuitively applied wrt some answer set of  if they are colored A8. Condition BTBD specifies that a rule D6 is colored A9 (not applied) if and only if D6 is not "grounded" (BTBDa) or D6 is blocked by some other rule (BTBDb). A rule is colored A8 (applied) if and only if it is grounded (BTBEa) and it is not blocked by some other rule (BTBEb) . This captures the intuition which rules apply wrt to some answer set and which do not (see Section 1).

Let D6 D4 BP D4 AW D2D3D8 D4. Then program  BP CUD6 D4 CV has block graph B4BN BNBN CUB4D6 D4 BN D6 D4 B5CVB5. By Definition 3.2 there is no a-coloring of A0  . For this reason, we need both conditions BTBD and BTBE.

Lemma 3.1 Let  be a logic program s.t. condition (4) holds and let CR be an a-coloring of A0  . Then condition BTBD holds iff condition BTBE does not hold.

In general, we do not have the equivalence stated in this lemma, because there are examples (see above) where no acoloring exists. Lemma 3.1 states that a-colorings are welldefined in the sense that they assign exactly one color to each node.

2 For a set of rules CB AI  we write CRB4CBB5 BP A8 or CRB4CBB5 BP A9 if for each D6BECB we have CRB4D6B5 BP A8 or CRB4D6B5 BP A9, respectively.

We obtain the main result:

Theorem 3.2 Let  be a logic program s.t. condition (4) holds and let A0  be the block graph of . Then  has an answer set BT iff A0  has an a-coloring CR. Furthermore, we have BZCAB4BN BTB5BPCUD6 BE  CY CRB4D6B5 BP A8CVBM

Answer sets can therefore be computed by computing acolorings, e.g. CRB4CUD6 CT CVB5 BP A9 and CRB4CUD6 CS BN D6 CQ BN D6 CR BN D6 CP BN D6 CU CVB5 BP A8 correspond to answer set BT BD of program (1).

4 Computation of A-colorings

For the following description of our algorithm to compute a-colorings, let  be some logic program s.t. condition (4) holds. Let CR BM  BJAX CUA9BNA8CV be a partial mapping. CR is represented by a pair of (disjoint) sets B4CR A9 BN CR A8 B5 s.t. CR A9 BP CUD6 BE  CY CRB4D6B5BPA9CV and CR A8 BP CUD6 BE  CY CRB4D6B5BPA8CV 3 . We refer to mapping CR with the tuple B4CR A9 BN CR A8 B5 and vice versa. Assume that A0  is a global parameter of each presented procedure (indicated through index ). Let CD and  be sets of nodes s.t. CD contains the currently uncolored nodes (CD BP  D2 B4CR A9 CJ CR A8 B5) and  contains colored nodes whose color has to be propagated. Figure 2 shows the implementation of the non-deterministic procedure color  in pseudo code.

procedure color  B4CDBN BM listBN CRBMpartial mappingB5 var D2 BM node ; if propagate  B4BN CRB5 fails then fail ; CD BMBP CD D2 B4CR A9 CJ CR A8 B5 ; if choose  B4CDBN CRBN D2B5 fails then CR BMBP B4CR A9 CJ CDBN CR A8 B5 ; if propagate  B4CDBN CRB5 fails then fail else output CR ; else CD BMBP CD D2 CUD2CV ; CR BMBP B4CR A9 BN CR A8 CJ CUD2CVB5 ; if color  B4CDBN CUD2CVBN CRB5 succeeds then exit else CR BMBP B4CR A9 CJ CUD2CVBN CR A8 D2 CUD2CVB5 ; if color  B4CDBN CUD2CVBN CRB5 succeeds then exit else fail ;

Notice that all presented procedures (except choose  ) return some partial mapping through parameter CR or fail. choose  returns some node or fails.

When calling color  the first time, we start with CR BP B4BNBN BY  B5, CD BP  D2 BY  and  BP BY  . That is, we start with all facts colored A8. Basically, color  takes both a partial mapping CR and a set of uncolored nodes CD and aims at coloring these nodes. This is done by choosing some uncolored node D2 (D2 BE CD) with choose  and by trying to color it A8 first. In case of failure color  tries to color node D2 with A9. If this also fails color  fails. Therefore, we say that node D2 is used as a choice point. All different a-colorings are obtained by backtracking over choice points.

choose  B4CDBN CRBN D2B5 selects some uncolored node D2 (D2 BE CD) s.t. AD A0 BC B4D2B5 BP BN and AD A0 BD B4D2B5 BIBP BN or the following condition holds:

BV there is some D2 BC BE AD A0 BC B4D2B5 s.t. CRB4D2 BC B5 BP A8.

3 Since CR is not total we do not necessarily have  BP CR A9 CJ CR A8 .

If there is no such D2 then choose  fails. This strategy to select choice points ensures that nodes CR A8 are grounded. Observe that, if choose  fails and CD BIBP BN then we have to color all nodes in CD with A9, since they cannot be grounded through rules CR A8 .

During recursive calls  contains the choice point of the former recursion level. The color of nodes  has to be propagated with propagate  (see Figure 3) for two reasons. First, when coloring nodes in  with color DC (DC BE CUA9BN A8CV) it is not checked whether this is allowed (wrt the actual CR). This check is done by propagate  . This means, color  fails only during propagation (see Theorem 4.1). Second, propagating already colored nodes prunes the search space and thus reduces the necessary number of choices. Since choice points make up the exponential part of our problem, propagation becomes the essential part of our approach.

Currently, we propagate only in arc direction as it is sufficient for correctness and completeness of the algorithm. Therefore, we have to deal with four propagation cases: if a node is colored DC (DC BE CUA9BNA8CV) then this color has to be propagated over 1- and over 0-arcs. Let D6 BC BN D6 BE  be nodes s.t. B4D6 BC BN D6B5 BE BT BC CJ BT BD and assume that D6 BC is already colored. Then we have to propagate this color to node D6. For example, propagating CRB4D6 BC B5 BP A8 over 1-arcs gives CRB4D6B5 BP A9. For reasons of correctness, we cannot propagate colors without any further tests. We have got the following result.

Theorem 4.1 Let  be a logic program s.t. condition (4) holds, let A0  be the corresponding block graph and let CR BM  BJAX CUA9BNA8CV be a mapping. If CR is an a-coloring of A0  then for each D6 BC BE  if D6 BC BE BY  then CRB4D6 BC B5 BP A8 and the following conditions hold:

(A) for each D6 BE AD B7 BD B4D6 BC B5 we have CRB4D6B5BPA9 if CRB4D6 BC B5BPA8 (B) for each D6 BE AD B7 BD B4D6 BC B5 we have CRB4D6B5BPA8 if CRB4D6 BC B5BPA9 and for each D6 BCBC BE AD A0 BD B4D6B5 BM CRB4D6 BCBC B5BPA9 and CJAD A0 BC B4D6B5 BP BN or there is some D6 BCBC BE AD A0 BC B4D6B5 BM CRB4D6 BCBC B5BPA8CL (C) for each D6 BE AD B7 BC B4D6 BC B5 we have CRB4D6B5BPA8 if CRB4D6 BC B5BPA8 and for each D6 BCBC BE AD A0 BD B4D6B5 BM CRB4D6 BCBC B5BPA9 (D) for each D6 BE AD B7 BC B4D6 BC B5 we have CRB4D6B5BPA9 if CRB4D6 BC B5BPA9 and for each D6 BCBC BE AD A0 BC B4D6B5 BM CRB4D6 BCBC B5BPA9.

According to Theorem 3.2, a rule contributes to some answer set BT if it is colored A8. In case of (A) there is no further condition, because a node D6 has to be colored A9 if there is some 1-predecessor D6 BCBC of D6 which is colored A8 (take D6 BCBC BP D6 BC in BTBDb Definition 3.2). In other words, D6 cannot be applied if it is blocked by some other applied rule. Intuitively, condition (B) says that D6 has to be applied if all of its 1-predecessors are colored A9 (D6 is not blocked) and one of its 0-predecessors is colored A8 (CQD3CSDD B7 B4D6B5 is a consequence of applied rules or D6 is a fact). Condition (C) states that rule D6 is applied if it is "grounded" through one of its 0-predecessors and if it is not blocked by some other rule. The last condition postulates that rule D6 cannot be applied if CQD3CSDD B7 B4D6B5 cannot be derived from other applied rules. Theorem 4.1 implies that a mapping CR is no a-coloring if propagate  fails. Figure 3 shows the implementation of propagate  . The purpose of propagate  is to

procedure propagate  B4 BM listBN CRBMpartial mappingBN) var D2 BC BM node ; while  BIBP BN do select D2 BC from  ; if B4D2 BC BE CR A8 B5 then (A ) if propA  B4D2 BC BN CRB5 fails then fail ; (C ) if propC  B4D2 BC BN CRB5 fails then fail ; else (B ) if propB  B4D2 BC BN CRB5 fails then fail ; (D ) if propD  B4D2 BC BN CRB5 fails then fail .

apply the corresponding propagation cases, e.g. if CRB4D2 BC B5 BP A8 then cases (A) and (C) have to be applied.

The four procedures used in propagate  can be easily implemented. For example, propB  is shown in Figure 4. First,

procedure propB  B4D2 BC BMnodeBN CRBMpartial mappingB5 var D2 BM node ; CB BM set of nodes ; CB BMBP CUD2 BE AD B7 BD B4D2 BC B5 CY condition (B) holds for D2CV ; while CB BIBP BN do select D2 from CB ; if D2 BE CR A9 then fail ; if D2 BIBE CR A8 then CR BMBP B4CR A9 BN CR A8 CJ CUD2CVB5 ; propagate  B4D2BN CRB5 .

it determines the set CB of all 1-successors of D2 BC s.t. condition (B) holds. Finally, it tests whether all nodes in CB can be colored A8. If node D2 BE CB is currently uncolored it is colored A8 and its color is propagated. If CRB4D2B5BPA9 then propB  fails, otherwise D2 is already colored A8 and we go on with the next node from CB. The procedures for the remaining propagation cases can be implemented analogously. Whenever some currently uncolored node is colored during propagation, this color is recursively propagated by calling propagate  .

For partial mapping CR BM  BJAX CUA9BNA8CV we define the set of corresponding answer sets BT CR as

BT CR BP CUCG CY CG is answer set of  and CR A8 AI BZCAB4BN CGB5 and CR A9 CK BZCAB4BN CGB5 BP BNCVBM

If CR is undefined for all nodes then BT CR contains all answer sets of . If CR is a total mapping then BT CR contains exactly one answer set of  (if CR is an a-coloring). With this notation we formulate the following result:

Theorem 4.2 Let  be a logic program s.t. condition (4) holds, let CR and CRB4D6B5 be partial mappings. Then for each D6 BE B4CR A9 CJ CR A8 B5 we have if propagate  B4CUD6CVBN CRB5 succeeds and CRB4D6B5 is the actual partial mapping after executing propagate  then BT CR BP BT CRB4D6B5 BM

This theorem states that propagate  neither discards nor introduces answer sets corresponding to some partial mapping CR. Hence, it justifies that only nodes used as choice points lead to different answer sets. Therefore backtracking is necessary only over choice points (see Figure 2).

Define BV  BP CUCR CY CR is some output of color  B4 D2 BY  BN BY  BN B4BNBN BY  B5B5CV. With this notation, we obtain correctness and completeness of color  .

Theorem 4.3 Let  be a logic program s.t. condition (4) holds, let A0  be its block graph, let CR BM  BJAX CUA9BNA8CV be a mapping and let BV  be defined as above. Then CR is an acoloring of A0  iff CR BE BV  .

Let us demonstrate how color  computes the a-colorings of the block graph of program (1) (see Figure 1). We invoke color  B4CDBNBN CRB5 with CD BP  D2 CUD6 CS CV,  BP CUD6 CS CV and CR BP B4BNBN CUD6 CS CVB5. First, propagate  B4BN CRB5 is executed. By propagating CRB4D6 CS B5 BP A8 with case (C) we get CRB4D6 CQ B5 BP A8 and recursively CRB4D6 CR B5 BP A8. This gives CR BP B4BNBN CUD6 CS BN D6 CQ BN D6 CR CVB5. After updating uncolored nodes we obtain CD BP CUD6 CP BN D6 CT BN D6 CU CV. Now choose  B4CDBN CRBN D2B5 (D2 variable) is executed. For choose  there are two possibilities to compute the next choice point s.t. BV hold, namely D6 CP and D6 CT . Assume D2 BP D6 CP . After updating CD we have CD BP CUD6 CT BN D6 CU CV and the first recursive call color  B4CDBN CUD6 CP CVBN CRB5 is executed where CR BP B4BNBN CUD6 CS BN D6 CQ BN D6 CR BN D6 CP CVB5. Again color A8 of node D6 CP has to be propagated by executing propagate  B4CUD6 CP CVBN B4BNBN CUD6 CS BN D6 CQ BN D6 CR BN D6 CP CVB5B5. By using propagation case (C) for CRB4D6 CP B5 BP A8 we obtain CRB4D6 CU B5 BP A8. This color is recursively propagated using case (A), which gives CRB4D6 CT B5 BP A9. This leads to CR BP B4CUD6 CT CVBN CUD6 CS BN D6 CQ BN D6 CR BN D6 CP BN D6 CU CVB5. Since CD becomes the empty set, choose  fails and CR is the first output. Invoking backtracking means that the last recursive call to color  fails. Then CR BP B4CUD6 CP CVBN CUD6 CS BN D6 CQ BN D6 CR CVB5 and color  B4CDBN CUD6 CP CVBN CRB5 is executed. By using case (D) for CRB4D6 CP B5 BP A9 we obtain CRB4D6 CU B5 BP A9 and thus CRB4D6 CT B5 BP A8 with case (B). Hence the second solution is CR BP B4CUD6 CP BN D6 CU CVBN CUD6 CS BN D6 CQ BN D6 CR BN D6 CT CVB5. Since there is no other choice point, we have no further solutions.

5 Generalizations

In this section, we discuss generalizations of the presented approach. First, we show how to apply our method to normal logic programs with multiple positive body literals. Let  be a normal programwithout restrictions. For each rule D6 BP D4 AW D5 BD BN BM BM BM BN D5 D2 BN D2D3D8 D7 BD BN BM BM BM BN D2D3D8 D7 CZ we define

where D5 BC BN D5 BC BD BN BM BM BM BN D5 BC D2 are new atoms not appearing in  . For a program  we set   BP CB D6BE  D6 . Hence, we have defined a local program transformation which has linear size of the original program. Each normal program is transformed into some program in which CQD3CSDD A0 B4D6B5 BP BN for each rule D6 with CYCQD3CSDD B7 B4D6B5CY BQ BD. That is why we may interpret   as some kind of normal form of . The following lemma obviously holds:

Lemma 5.1 Let  be a normal logic program and let BT be a set of atoms. Then BT is an answer set of  iff there exists an answer set BT  of   s.t. BT and BT  contain exactly the same atoms out of the set of all atoms occurring in  .

It is straightforward to extend the algorithm presented in Section 4 to normal programs   . Let us call all rules D6 BE   with CYCQD3CSDD B7 B4D6B5CY BQ BD AND-nodes and all other rules ORnodes. Observe, that on the one hand, we do not have to modify Definition 3.1 of block graphs for programs   . It stays as it is. We just distinguish two different kinds of nodes in A0   . On the other hand, Definition 3.2 and procedures presented in Section 4 deal only with OR-nodes and consequently we have to extend it to AND-nodes. For AND-node D6 we know by definition that AD A0 BD B4D6B5BPBN (see (5)). Therefore, D6 cannot be blocked and we do not have to consider cases BTBDb and BTBEb of Definition 3.2. In order to extend Definition 3.2, we require that the following conditions hold for each AND-node D6 (corresponding to conditions BTBDa and BTBEa of Definition 3.2 for OR-nodes):

According to (5), for AND-node D6 we have AD A0 BD B4D6B5BPAD B7 BD B4D6B5BP BN, CYAD B7 BC B4D6B5CYBPBD and AD B7 BC B4D6B5CJAD A0 BC B4D6B5 will never contain any ANDnode. For this reason, we obtain only two new propagation cases, in which we propagate the color of OR-nodes over 0arcs to AND-nodes. Let D6 BE AD B7 BC B4D6 BC B5 be some AND-node and let DC BE CUA9BNA8CV be the actual color of D6 BC (OR-node). Then we have the following new cases

which can be easily integrated into propagate  .

[Gelfond and Lifschitz, 1990] show that logic programs with classical negation are equivalent to normal logic programs when new atoms are introduced. With this technique our approach is also suitable for computing answer sets of general logic programs (with classical negation). Additionally, we may apply techniques presented in [Janhunen et al., 2000] to handle disjunctive logic programs.

6 RelatedWork

Directed graphs are often associated with logic programs and used in theory and applications. Usually, the nodes of these graphs are the atoms of the programs, e.g. dependency graphs or TMS networks [Doyle, 1979] 4 . These approaches use rules to define graphs on atoms whereas we have used atoms to define graphs on rules.

Other approaches [Dimopoulos and Torres, 1996; Brignoli et al., 1999] are more or less rule-based but have some serious drawbacks: they deal only with prerequisite-free programs, because (wrt to answer set semantics) there is some equivalent prerequisite-free program for each program. Since in general equivalent prerequisite-free programs have exponential size of the original ones, approaches which rely on this equivalence need exponential space.

In fact, the block graph is a specialization of graphs defined on rules in [Papadimitriou and Sideri, 1994; Linke and Schaub, 2000] for default theories. Whereas in the case of default logic the aforementioned graphs are abstractions of the essential blocking information, here they contain all information necessary for computing answer sets. Although we focus on the practical usage of the block graph it may also be used as a tool for theoretical analysis of logic programs. For example, results presented in [Linke and Schaub, 2000] imply that a logic program without odd cycles always has some answer set.

4 Truth maintenance systems can be translated into logic programs [Brewka, 1991].

Clearly, color  is, like smodels, a Davis-Putnam like procedure. Once again, the main difference is that color  determines answer sets in terms of generating rules whereas smodels and dlv construct answer sets in terms of literals. Using rules instead of atoms has the advantage that we have complete knowledge about which rule is responsible for some atom belonging to an answer set. Atom-based approaches additionally have to detect the responsible rule and ensure groundedness, because in general there may be several rules with the same head. We obtain groundedness of generating rules as a by-product of our strategy to select choice points with procedure choose  .

7 Conclusion

The main contribution of this paper was the definition of the block graph A0  of a program . As a theoretical tool, the block graph seems to be suitable for investigations of many concepts for logic programs, e.g. answer set semantics, wellfounded semantics or query-answering. As a first result, we have described answer sets as a-colorings (a non-standard kind of graph colorings of A0  ). This led us to an alternative algorithm to compute answer sets by computing a-colorings which needs polynomial space.

Finally, let us give first experimental results to demonstrate the practical usefulness of our algorithm. We have used two NP-complete problems proposed in [Cholewi´nski et al., 1995]: the problem of finding a Hamiltonian path in a graph (Ham) and the independent set problem (Ind).

Concerning time, our first prolog implementation (development time 6 month) is not comparable with state of the art implementations. However, Theorem 4.2 suggests to compare the number of used choice points, because it reflects how an algorithm deals with the exponential part of a problem. Unfortunately, only smodels gives information about its choice points. For this reason, we have concentrated on comparing our approach with smodels. Results are given for finding

all solutions of different instances of Ham and Ind. Table 1 shows results for some Ham-encodings of complete graphs  D2 where D2 is the number of nodes 5 . Surprisingly, it turns out that our non-monotonic reasoning system (noMoRe) performs very well on this problem class. That is, with growing problem size we need less choice points than smodels. This can also be seen in Table 2 which shows the corresponding time measurements. For finding all Hamiltonian cycles of a  BDBC we need less time than the actual smodels version. To be fair, for Ind-problems of graphs Cir D2 6 we need twice the choice points (and much more time) smodels needs, because we have not yet implemented backward-propagation. However, even with the same number of choice points smodels is faster than noMoRe, because noMoRe uses general backtracking of prolog, whereas smodels backtracking is highly specialized for computing answer sets. The same applies to dlv.

5 In a complete graph each node is connected to each other node.

6 A so-called circle graph Cir D2 has D2 nodes CUDA BD BN BM BM BM BN DA D2 CV and arcs BT BP CUB4DA CX BN DA CXB7BD B5 CY BD AK CX AK D2CV CJ CUB4DA D2 BN DA BD B5CV.

For future work, we may also think of different improvements of our algorithm. First of all, we have to integrate backward propagation (propagating colors against arc direction), since this will definitely improve efficiency by further reducing the number of choice points. Second, we may try to pre-color not only facts but also some other nodes, e.g. each node D2 with B4D2BN D2B5 BE BT BD has to be colored A9. The block graph may also be used for other improvements. For example, it is possible to replace 0-paths without incoming and outgoing 1-arcs by only one 0-arc. Finally, we have to investigate different heuristics for procedure choose  to select the next choice point.

The approach as presented in this paper has been implemented in ECLiPSe-Prolog [Aggoun et al., 2000]. The current prototype is available at http://www.cs.unipotsdam.de/˜linke/nomore.

Acknowledgements

I would like to thank T. Schaub, Ph. Besnard, K. Wang, K. Konczak, Ch. Anger and S.M. Model for commenting on previous versions of this paper.

This work was partially supported by the German Science Foundation (DFG) within Project "Nichtmonotone Inferenzsysteme zur Verarbeitung konfligierender Regeln".