On Tight Logic Programs and Yet Another Translation from Normal Logic Programs to Propositional Logic

1 Introduction

It is well-known that a stable model of a logic program is also a logical model of the completion of the logic program, but the converse is not true in general. However, Fages [ 1994] showed that if the program is tight (i.e. it has no positive loops), then the converse is also true. Recently, Babovich, Erdem, and Lifschitz [2000] generalized Fages' result, and showed that the converse is also true if the pro­ gram is tight on the given model of the completio~. As it turned out, this is quite a general result as many mterest­ ing logic programs are indeed tight on every model of their completions. In fact, among the commonly known bench­ mark domains, only Niemela's normal logic program en­ coding of the Hamiltonian Circuit (HC) problem [Niemela,

*Corresponding author

1999] is not tight on its completion models. This leads nat­ urally to the question: is there a normal logic program en­ coding of the HC problem that is tight on every model of its completion? At first glance, a positive answer seems eas­ ily followed from some known results. For instance, us­ ing any of the known transformation from logic programs to propositional theories (e.g. [Ben-Eliyahu and Dechter, 1996; Lin and Zhao, 2002]), one can translate a program to a set of clauses, and then back to a logic program that is tight (on every model of the program's completion). While this is cer­ tainly true, it is not really what we wanted. Given a graph, a logic program for solving the HC problem for the graph normally should have two parts - a set of facts that defines the graph in terms of vertices and edges, and a set of general rules. While the above reasoning shows that it follows from the known results that for any given graph, a tight logic pro­ gram can be found for solving the HC problem on the graph, it does not follow, although it is true as we shall show in this paper, that there is a set of general rules such that for any given graph, the logic program consisting of the set of gen­ eral rules and the set of facts encoding the graph is always tight.

By modifying Niemela's encoding, we propose a new nor­ mal logic program for solving the HC problem, and show that the program is tight on every model of its completion. Compared with Niemela's encoding, our new encoding yields much larger programs - about twice more atoms and rules. Surprisingly, despite its larger size, for both SMODELS [Si­ mons, 2003] and ASSAT [Lin and Zhao, 2002], the new en­ coding performs better 1 on many randomly generated graphs. For ASSAT, it also performs better on complete graphs, which are hard for SMODELS and ASSAT partly because of the sizes of the programs corresponding to these graphs. However, our new encoding is slower than Niemela's on some of the hand-coded hard graphs in [Lin and Zhao, 2002], which are constructed by taking a few copies of a graph and con­ necting these copies by some arcs. While these experimental results are mixed, they do suggest that it is worthwhile to try to encode a problem as a logic program whose stable models are the same as its completion models.

This motivated us to investigate a sufficient and necessary condition for a completion model to be a stable model. To this end, we generalize the notion of tight on a set of atoms into that of inherently tight on a set of atoms. Specifically, we call a program P inherently tight on a set S of atoms if there is a subprogram Q <::; P such that S is a stable model of Q and Q is tight on S . We show that for any program, a completion model of this program is also its stable model iff the program is inherently tight on the model.

1 All performances in this paper are about computing one stable

model of a program.

We then propose a polynomial transformation from any logic program to one that is inherently tight on all its com­ pletion models. This provides a reduction of stable model se­ mantics to completion semantics and SAT. Compared to the one in [Ben-Eliyahu and Dechter, 1996] which needs n 2 ex­ tra atoms and n 3 new rules, and the one in [Lin and Zhao, 2002] which does not introduce any new atom but in the worst case may add an exponential number of new rules (clauses), our transformation introduces O(n 2 + m) extra atoms and O(n x m) extra rules in the worst case, where n is the num­ ber of atoms in the original program and m the number of rules. We have observed that in all of the benchmark logic programs, the number of rules in a program is smaller than n 2 . One useful feature of our transformation is that it is mod­ ular w.r.t adding new facts.

This paper is organized as follows. Section 2 introduces some logical preliminaries. Section 3 studies an encoding of the HC problem that is tight on every completion model of the program, and reports some experimental results using SMODELS and ASSAT(Chaff2) . Section 4 proposes a notion of inherent tightness and a translation from a logic program to one that is inherently tight. Section 5 concludes this paper. Due to space limitations, proofs, if given, are only sketched.

2 Logical Preliminaries

Logic programs A normal logic program is a set of rules of the following form:

where a is either an atom or empty, b's, and c's are atoms. When a is empty, then the rule is a constraint, and when m = n = 0 and a is an atom, then the rule is a fact, asserting that a is true. Given a ruler, in the following, we denote by H ead(r) its head atom, and Pos(r) and Neg(r) the set of positive body literals and the set of atoms that occur under not in the body of rule r, respectively. For any set X of atoms, we denote the set {not L: LEX} by not(X). So a rule r can be represented as

Given a program P, in the following, we let Atom(P) be the set of atoms in P.

Program completion Given a logic program P, its comple­ tion, Comp(P) is the union of the constraints in P and the Clark completion [Clark, ] of P with constraints deleted. In other words, it consists of the following sentences:

• For any atom a, if a +-- G1 , · · ·,a +-- Gn are all the rules about a in P, then a ::= G1 V · · · V Gn is in Comp(P) . Here we abuse the notation and write Gi both as the

body of a rule and a disjunct in a formula. Its intended meaning is that when we write a body G in a formula, it stands for true if G is empty, it is the conjunction of literals in G with not replaced by · otherwise. Notice here that when n = 0, the equivalence for a becomes a == fal se;

• If+-- G is a constraint in P , then -,Q is in Comp(P ).

The stable model semantics Given a logic program P without constraints, and a set S of atoms, the Gelfond­ Lifschitz transformation of PonS, written asPs, is obtained from P as follows:

• For each atom q and any ruler in P, if q E Neg(r) and q rf. S, then delete the literal not q from the body of ruler.
• In the resulted set of rules, delete all those rules that still contain a negative literal in their bodies, i.e., for any rule r E P , if there is a q E N eg(r) such that q E S, then delete this ruler.

It is clear that for any set of atoms S, Ps is a set of rules without any negative literals. Thus Ps has a unique mini­ mal model, which is the same as the set of atoms that can be derived from the program by resolution when rules are inter­ preted as implications. We denote this set as Cons(Ps ). A setS is a stable model [Gelfond and Lifschitz, 1988] of P if and only if S = Cons(Ps ).

Now let P be a program that may have constraints, and P' the result of deleting all constraints in P. Then a set of atoms is a stable model of P iff it is a stable model of P' and satis­ fies all the constraints in P.

Dependency graph The predicate dependency graph [Apt et al., ] of a logic program P is a directed graph with signed edges. The vertices are atoms mentioned in P. There is a directed positive (resp. negative) edge from vertex p to q if there is a ruler in P such that H ead(r) = q and p E Pos(r ) (resp. H ead(r) = q and p E N eg(r)) . Informally, a posi­ tive (resp. negative) edge from p to q means that q depends positively (resp. negatively) on p.

For any two atoms a and f3 in P, there is a positive path from a to f3 if and only if there is a path from vertex a to vertex f3 in the dependence graph G p and the path has no negative edges.

3 Tight logic programs and Hamiltonian Circuit problem

A program P is tight [Lifschitz, 1996] if there exists a level mapping >. such that, for every rule

inP,

Here a level mapping is a function from literals to ordinals.

It is not hard to see that a program is tight iff its dependency graph has no positive cycles. For these programs, the program completion semantics under classical logic coincides with the stable model semantics. That is, if a program is tight, then a set of atoms is its stable model iff it is a classical propositional model of its completion [Fages, 1994]. Recently, Babovich, Erdem, & Lifschitz [2000] generalized this result to "tight on a set of literals" by modifying the mapping>. to a partial level mapping with respect to a set of literals. Formally, a program P is tight on a set S of atoms if there exists a partial level mapping >. with the domain S such that, for every rule (3) in P, if a and b1 , · · ·, bk E S, then

They showed that if a normal logic program is tight on a model of its completion, then this model is also a stable model. As a result, if the logic program is tight or tight on all models of its completion, to find stable models of this logic program, we can reduce it to SAT by computing its completion. As it turned out, this is quite a general result as many interesting logic programs, including all constraint sat­ isfaction problems and planning problems are indeed tight on every model of their completions. In fact, among the commonly known benchmark domains, only Niemela's nor­ mal logic program encoding of the Hamiltonian Circuit (HC) problem [Niemela, 1999] is not always tight on its completion models.

As the experimental results reported in [Babovich et al., 2000; Huang et al., 2002; Lin and Zhao, 2002] showed, for problems like graph coloring and blocks world planning whose encodings in logic programs are either tight or tight on their completion models, computing a stable model of these programs using the state of art SAT solvers on their com­ pletions is a lot faster than SMODELS, which is currently the state of art specialized stable model generator for normal logic programs. For HC problems, while ASSAT still outper­ forms SMODELS, the improvements are not as great as in other problems. One of the reasons is that when a completion model may not be a stable model, ASSAT needs to repeatedly call a SAT solver, and the total computation time is directly proportional to the number of times a SAT solver is called. So to see if this was due to the inherent difficulty of the HC problem or because of the particularity of Niemela's encod­ ing [Niemela, 1999], we came up with an encoding of the HC problem that is always tight on the completion models.

To motivate our new encoding, let's first look at Niemela's given below:

As one can see, rules (6) - (8) guess some paths with the property that for every vertex X, if X has at least one out­ going arcs, then exactly one of these arcs is chosen to be in the paths, and similarly if X has at least one incoming arcs, then exactly one is chosen to be in the paths. The rest of the rules then make sure, especially by asserting that reached(X) must be true for every vertex X, that these paths are in fact a single simple cycle that covers the whole graph. When grounded, this program is not tight because rule (9) would create cycles among reached( X) atoms.

Another way of solving the problem is to first guess some paths that must go through every vertex exactly once, and then make sure that when we do not count the outgoing arc from the starting vertex, these paths are in fact a single path that does not contain any cycles. This is the idea behind our program in Figure 1 for solving the HC problem:

Figure 1: An encoding of the HC problem that is always tight on every model of its completion

Notice that rules (16)- (18) are the same as (6)- (8); rules (12)- (15) are needed to make sure that the chosen path must go through each vertex exactly once for the cases when aver­ tex has no outgoing (incoming) arcs in the graph; rules (19) - (21) use the binary predicate reached(X, Y) to make sure that when we delete the chosen outgoing arc from the starting vertex, the chosen path has no cycles, thus must be a single path. Formally, it can be shown that the program correctly solves the HC problem and is always tight on every comple­ tion model.

Proposition 1 Let G = (V, E) be a graph. Let P be the union of the rules in Figure 1 and facts represented by the graph in terms of vertex( X) and arc( X, Y). If M is a stable model of P, then atoms of the form he( u, v) in M correspond to an HC of G. Furthermore, P is tight on every model of its completion.

Given a graph, compared with Niemela's encoding, ours yields a larger program because reached in our program is a binary predicate. To evaluate the performance of this program, we tried SMODELS (version 2.27) and AS­ SAT(Chaff2) (version 1.3 with its simplification feature ac­ tivated) on the same set of graphs 2 used in [Lin and Zhao,

2 These graphs can be downloaded from ASSAT's web site http://www.cs.ust.hk/assat.

2002], which divided it into three categories: randomly generated graphs, hand-coded hard instances, and complete graphs. Our experiments were done on Sun Ultra 5 machmes with 256M memory running Solaris. The times given be­ low are in CPU seconds as reported by Unix "time" com­ mand, and include the times for running !parse for grounding the input programs. For randomly generated graphs (see Ta­ ble 1), ASSAT clearly performs much better using our new encoding; SMODELS also seemed to behave better using the new encoding as the run times are more uniform now. How­ ever, for hand-coded graphs (see Table 2), which are formed by first taking several copies of a small graph and then se­ lectively adding some arcs to connect these components, the old encoding was clearly better for SMODELS. For ASSAT, some of the graphs became easier with the new encoding, but many became harder. Finally, for complete graphs, which are hard partly because they yield huge programs both for the new and old encodings, the new encoding turned out to be better for ASSAT but a little worse for SMODELS. For in­ stance, for the complete graph with 80 vertices, using the old encoding, ASSAT returned with a solution in 3297 seconds, and SMODELS in 5072 seconds, but with the new encoding, ASS AT took only 170 seconds, but SMODELS needed 12485 seconds.

From these mixed results, it seems that both encodings have merits, especially if one uses SMODELS. But the ex­ periments do suggest that the new encoding, being tight on every completion model, is better for SAT-based stable model generators such as ASS AT and Cmodels 3 . We would not be surprised that with better and faster SAT solvers, the new en­ coding would outperform in all cases.

4 Inherently tight programs

Given the potential benefit of tight logic programs for SAT­ based stable model generators, we now investigate a. more general translation from an arbitrary logic program to o~e whose completion models are always stable models. To this end, we first define a notion of inherently tight on a set of atoms, and show that it is a sufficient and necessary condition for a program's completion model to be a stable model.

Definition 1 A program P is inherently tight on a set of atoms S if there is a program Q such that Q ~ P, S is a stable model ofQ and Q is tight on S.

Proposition 2 A normal logic program is inherently tight on all of its stable models.

Proof: Suppose S is a stable model of P. Notice first that each rule in Ps has a corresponding one in P under Gelfond­ Lifschitz transformation. Now define W, a set of rules, as follows:

1. W is initially empty, and T initially Ps;

3 We also ran experiments for Cmodels (http://www.cs.utexas.edu/users/tag/cmodels.html). The results were very similar to the ones for ASS AT. We did not include its data here because it is not guaranteed to work when the input program is not tight, like Niemela's encoding of the HC problem here.

1. Choose a fact a <-in T. Suppose r is the corresponding rule in P. Now let W be W U r, and remove all rules about a from T, and delete a in the bodies of all other rules in T;
2. Go back to Step 2 until T is empty.

It is clear that W is tight and S is one of its stable models. Thus Pis inherently tight on S. ·

Theorem 1 Let P be a normal logic program, and S a set of atoms. Then S is a stable model of P if and only if S is a model of the completion of P and P is inherently tight on S.

Proof: ::::?: By Proposition 2 and the fact that a stable model is also a model of a program.

<=: Since S be a model of the completion of P, so S is closed under P. Since P is inherently tight on S, there is a Q ~ P such that S is a stable model of Q and Q is tight on S. Thus Sis supported by Q, hence also supported by P. Now S is supported by and closed under P, thus a stable model of P (by a theorem in [Babovich et al., 2000]). ·

We say that a program is inherently tight if it is inherently tight on all models of its completion. Clearly, a program that is tight on all its completion models is inherently tight. By Theorem 1, if all models of its completion are also its stable model, then the program is inherently tight, and vice versa.

We now give a translation from an arbitrary logic program to one that is inherently tight. · In the following, a set S of atoms in a program P is called a strongly connected com­ ponent (SCC) if there is a path in G p from u to v for any u, v E S, and S is not a subset of any other such set, where G p is the dependency graph of P.

Algorithm 1 Let P be a normal logic program. the following algorithm transforms it to an inherently tight program Q. Let Q be empty initially.

1. For any ruler E P of the form

b; (1 ::::; i ::::; n) and atom a are in the same sec while dj (1 ::::; j ::::; m) and a are not. We add the following rules into Q:

In these rules, 1 ::::; i ::::; nand variable X will be instan­ tiated to all atoms a if a and a are in the same SCC;

1. If r E P is a constraint, add rule r it into Q.

Intuitively, if a set M is a stable model of Q, then ar E M iff a E M and the ruler in P 'contributes' to the calculation of Cons ( Q M), meaning that rule r is actually used to derive a. right(u, v) is used to record that atom u is used to prove v and this is needed to prevent loops. The following example illustrates the idea.

Example 1 Consider the program P = {a <- b. b <­ a. a <- not c. c <- c.}. It has two completion models {a, b} and { c }, but only the first one is a stable model. For this program, there are two SCCs: {a, b} and { c }. Algorithm I transforms it into the following program Q:

The completion of the program contains the following equiv­ alences c :=c1, c1 = ·right(c, c) 1\ c, and right(c, c) = c1. Thus it entails ·c 1\ ·c1 1\ ·right( c, c). So there is only one model of the completion where a and bare true and cis false, which is also the only stable model of Q. Notice that in the stable model of P, a is established by the second rule about it. Correspondingly, in the stable model ofQ, a2 is true while a1 is not, and right( a, b) is true while right(b, a) is not (a is established first, and then b is derived from a).

Theorem 2 For any normal logic program P, the program Q output by Algorithm 1 is inherently tight. Furthermore P and Q are equivalent on Atom(P), that is, for any subsetS of Atom(P), Sis a stable model of P iff there is exactly one stable modelS' of Q such that such that S = S' n Atom( P).

Proof: We show only that Q is inherently tight. The second part of the theorem is easier.

We only need to prove that all models of Camp( Q) are its stable models. Let N be a model of the completion of Q. We show that N satisfies every loop formula of Q, thus it must be a stable model of Q (Theorem 1 in [Lin and Zhao, 2002]) Suppose L is a positive loop in Q. According to Algorithm 1, either L is a loop that does not contain any atom of the form right( u, v) or L is a set of atoms of the form right( u, v).

If L is a loop that does not contain any atom of the form right(u, v), suppose v1 , · · ·, Vs are all atoms in L. L has even number of atoms. Atoms in Atom(P) and newly added atoms occur along the loop alternatively. Suppose the loop is: xi, x1, x2, x2, · · · , x~, Xt where x~ are newly added atoms and Xi are atoms in Atom(P) (1 ::::; i ::::; t). If all Vj (1 ::::; j ::::; s) are inN, it is known that right(x;, Xi+!) are inN by rule 25. Further considering rule 26, we have right( xi, Xi-d E N for some i, thus rule 23 can not be satisfied for some x~

in the loop. So not all atoms in the loop are inN. Now that N is a model of the completion, so the loop formula [Lin and Zhao, 2002] for loop L is satisfied.

If L is a loop and it contains a set of atoms right( a!, a2), right(a2, a3), · · ·, right(av, a1). Sup­ pose right( a, b) is an atom in L and it is deduced by the rule right( a, b) +- bi , right( a, c) . Suppose there is a ruler such that Pos(r) n L = 0, if Body(r) is satisfied by N, the loop formula of L is satisfied. If there is no such a r, then the rule right( a, b)+- bi, right( a, c) must be satisfied. Thus bi E N. But there is only one rule about bi which requires right( a, {3) rf. N for some a, {3 E L for it to be applicable. However from our assumption that L ~ N, and L is a loop, it must be the case that right( a , {3 ) E N for all a , {3 E L. This is a contradiction, thus there must be an r as above. ·

Algorithm I effectively provides yet another reduction of answer set semantics to SAT by calculating the completion of the translated program. Compared with the mapping in [Ben-Eiiyahu and Dechter, 1996], which always adds n 2 ex­ tra atoms and n 3 extra rules, the number of extra atoms and rules needed for our transformation depends on the number of rules whose heads and some of positive literals in their bodies belong to the same SCC. In the worst case, it needs 0 ( n 2 + m) extra atoms and 0 ( n x m) extra rules, where n is the number of atoms and m the number of rules in the input program. Usually, m is a lot less than n 2 . For instance, for Niemela's encoding of the HC problem, given a iraph with k vertices, there are at most O(k 2 ) atoms and O(k ) rules.

One interesting feature of Algorithm I is that it is modular w.r.t. new facts. That is, if P' is a set of facts, then for any program P, the program returned by the algorithm on P U P' is the union of the programs returned by it on P and P'. This feature will be handy when we extend the algorithm to programs with variables as the instantiation of a program with variables can be thought of as the union of the program and a set of ground facts.

We have implemented the algorithm and tried it on Niemela's encoding of the HC problem, and found that for SMODELS, the translated program is still better than the original one on randomly generated graphs. But on other types of graphs, the translated program is a lot worse. But for ASSAT, the translated program was slower even on ran­ domly generated programs. Apparently, being (inherently) tight does not always guarantee better performance even for SAT-based stable model generators.

5 Conclusions and future work

We have proposed a new solution to the Hamiltonian Circuit problem. For any given graph, the solution yields a program that is tight on every model of its completion. Compared with Niemela's encoding of the same problem, our new encod­ ing performs better on both randomly generated graphs and complete graphs, but is slightly worse on a set of hand-coded graphs. While these results hold for both SMODELS, which is a specialized stable model generator, and ASSAT, which makes use of SAT solver Chaff2, the performance gain seems greater for ASSAT than for SMODELS.

We also defined a notion of inherent tightness that captures a sufficient and necessary condition for a program completion model to be its stable model, and proposed an algorithm for translating an arbitrary logic program into an inherently tight one, which provides a reduction of stable model semantics to completion semantics and SAT.

In terms of future work, we are interested in finding out more about the relationships between stable model semantics and completion semantics, especially the kinds of features of an inherently tight logic program that would be particularly good for SAT-based stable model generators like ASSAT.

Acknowledgements

We thank Yuting Zhao for useful discussions. related to the topics of this paper, especially for his helps in using AS SAT, and for providing some experimental data on AS SAT.

This work was supported in part by the Research Grants Council of Hong Kong under Competitive Earmarked Re­ search Grant HKUST6205/02E.