Stable Model Checking Made Easy

1 Introduction

Disjunctive logic programming (DLP) with stable model semantics is a powerful nonmonotonic formalism for knowledge representation and commonsense reasoning [Baral and Gelfond, 1994; Lobo et. al., 1992]. DLP has a very high expressive power [Eiter et. al., 1997a], and it allows to represent complex problems in a simple and easy-to-understand fashion [Eiter et. al. , 1998]. As for the other main nonmonotonic formalisms, reasoning with DLP (under stable model semantics) is very hard. The high complexity of DLP reasoning depends also on the hardness of stable model checking- deciding whether a given model is a stable model of a propositional DLP program - which is co-NP-complete. The hardness of this problem has discouraged the implementation ofDLP engines. Indeed, at the time being only one system, namely the dlv system [Eiter et. al., 1998], is avail­ able which fully supports (function-free) DLP with sta­ ble model semantics.

*Research supported by FWF (Austrian Science Fund) under the projects P11580-MAT and Z29-INF.

This paper proposes a new transformation, which re­ duces stable model checking to UNSAT - i.e., to decid­ ing whether a given CNF formula is unsatisfiable - the complement of Satisfiability, a problem for which very efficient systems have been developed in AI.

Besides providing an elegant characterization of stable models which sheds new light on their intrinsic nature, the pr;posed transformation has also a strong practical impact. Indeed, by using this transformation, the huge amount of work done in AI on the design and implemen­ tation of efficient algorithms for checking Satisfiability can be profitably used for the implementation of DLP engines supporting stable model semantics. Thus, this transformation opens "new frontiers" in the implementa­ tion of Disjunctive Logic Programming which can benefit now from efficient AI techniques and implementations.

We have implemented the proposed technique in the DLP system dlv, and we have run a number of experi­ ments and benchmarks.

In sum, the main contributions of this paper are the following:

• We define a new transformation from stable model checking for general DLP with negation to UNSAT of propositional CNF formulas. The transformation is par­ simonious (i.e., it does not add any new symbol) and efficiently computable, since it runs in logspace (and, therefore, in polynomial time). Moreover, the size of the generated CNF formula never exceeds the size of the in­ put (it is usually much smaller).
• We realize our approach in the DLP system dlv, by using an implementation of the Davis-Putnam procedure as the Satisfiability checker.

Our implementation exploits also novel modular eval­ uation techniques, which follow from our main results.

• We carry out an experimental activity which witnesses the efficiency of our approach to stable model checking.

It is worth noting that, since stable model checking of DLP programs generalizes minimal model checking for Horn CNF formulas, our results can be employed also for reasoning with minimal models and with circumscrip­ tion.

The dl v system, which implements the results described in this paper, can be downloaded from www.dbai.tuwien.ac.at/proj/dlv. From the same Web page, one can also retrieve the benchmark prob­ lems that we used in our experiments.

The remainder of the paper is organized as follows: Setions 2 and 3 contain preliminary notions on DLP, stable model semantics, and its characterization in terms of unfounded sets. Section 4 describes our new reduction from stable model checking 'to UNSAT. Section 5 reports on our experiments.

2 Disjunctive Logic Programming with Stable Model Semantics

In this section, we provide an overview of disjunctive logic programming with stable model semantics. (For further details, see [Lobo et. al., 1992].)

The terms of the language are inductively defined. A variable or constant is a term; a function symbol with terms as arguments is a term. An atom is a(t1, ... , tn) , where a is a predicate of arity n and h, ... , tn are terms. A literal is either a positive literal p or a negative literal -.p, where p is an atom.

A (disjunctive) rule r is a clause of the form

where a1 , ···,an, b1 , · · ·, bm are atoms. The disjunction a1 V · · · V an is the head of r, while the conjunction b1 1\ ... 1\ bk 1\ -.bk+l 1\ .. . 1\ -.bm is the body of r. We de­ note by H ( r) the set { a1 , ... , an} of the head atoms, and by B(r) the set {bl, ... ,bk,-.bk+l, ... ,-.bm} of the body literals. B+(r) (resp., B - (r)) denotes the set of atoms occurring positively (resp., negatively) in B(r). A (dis­ junctive) program (also called DLP program) is a set of rules. A -.-free (resp., V-free) program is called positive (resp., norma0. A term, an atom, a literal, a rule, or a· program is ground if no variables appear in it. A finite ground program is also called a propositional program. A function-free program is a finite program where no function symbol occurs.

Let P be a program. The Herbrand universe and the Herbrand base of P are defined in the standard way and denoted by Up and Bp, respectively. Given a rule r occurring in a P, a ground instance of r is a rule obtained from r by replacing every variable X in r by a(X), where a is a mapping from the variables occurring in r to the terms in Up. We denote by ground(P) the set of all the ground instances of the rules occurring in P.

An interpretation for P is a set of ground atoms, that is, an interpretation is a subset I of Bp. A ground posi­ tive literal A is true (resp., false) w.r.t. I if A E I (resp., A ¢ I). A ground negative literal -.A is true w.r.t . I if A is false w.r.t. I ; otherwise -.A is false w.r.t. I.

Let r be a ground rule in ground(P). The head of r is true w.r.t. I if H(r) n I =f:. 0. The body of r is true w.r.t. I if all body literals of r are true w.r.t. I (i.e., B+(r) <;;;; I and B-(r) n I =f:. 0) and is false w.r.t. I otherwise. The ruler is satisfied (or true) w.r.t. I if its head is true w.r.t. I or its body is false w.r.t. I .

A model for P is an interpretation M for P such that every ruler E ground(P) is true w.r.t. M. A model M for P is minimal if no model N for P exists such that N is a proper subset of M. The set of all minimal models for Pis denoted by MM(P).

A generally acknowledgeq semantics for DLP pro­ grams is the extension of the stable model semantics to take into account disjunction [Gelfand and Lifschitz, 1991; Przymusinski, 1991]. Given a program P and an interpretation I, the Gelfond-Lifschitz (GL) transforma­ tion of P w.r.t. I , denoted pi , is the set of positive rules defined as follows:

Definition 2 1 [Przymusinski, 1991; Gelfond and Lif­ schitz, 1991] Let I be an interpretation for a program P. I is a stable model for P if I E MM(PI) (i.e., I is a minimal model of the positive program pi). 0

Example 2.2 Let P = {a V b ,_ c; b ,_ -.a 1\ -.c; a V c ,_ -.b} and I = { b}. Then, pi = {a V b ,_ c; b ,_ }.

It is easy to verify that I is a minimal model for pi; thus, I is a stable model for P. 0

Clearly, if P is positive, then pi coincides with ground(P) . It turns out that for a positive program, minimal and stable models coincide.

3 Stable Models and Unfounded Sets

Next , we present a characterization of the stable mod­ els of disjunctive logic programs in terms of unfounded sets. This characterization will be used to prove the cor­ rectness of our reduction from stable model checking to UNSAT in the next section.

The characterization presented here is obtained by slight modifications of the results presented in [Leone et. al., 1997]. In particular, providing the notion of un­ founded sets directly for total (2-valued) interpretations, we obtain a simpler characterization than in [Leone et. al., 1997], where unfounded sets were defined w.r.t. par­ tial (3-valued) interpretations.

Definition 3.1 (Definition 3.1 in [Leone et. al., 1997]) Let I be an interpretation for a program P. A set X <;;;; Bp of ground atoms is an unfounded set for P w.r.t. I if, for each ruler E ground(P) such that X n H(r) =f:. 0, at least one of the following conditions holds:

1. (B+(r) g I) V (B-(r) n I =f:. 0), that is the body of r is false w.r.t. I.
2. B+(r) n X =f:. 0, that is, some positive body literal belongs to X.
3. (H(r)- X) n I =f:. 0, that is, an atom in the head of r, distinct from the elements in X, is true w.r.t. I. 0

Input: A ground DLP program Panda model M for P. Output: A propositional CNF formula fM(P) over M . var P': DLP Program; S: Set of Clauses; begin

1. Delete from P each rule whose body is false w.r.t. M;
2. Remove all negative literals from the (bodies of the) remaining rules;
3. Remove all false atoms (w.r.t . M) from the heads of the resulting rules;
4. s := 0;
5. Let P' be the program resulting from steps 1-3;
6. for each rule a1 V · · · V an +- b1 1\ · · · 1\ bm in P' do

7.

S := S U { b1 V · · · V bm +- a1 1\ · · · 1\ an };

1. end for;
2. rM(P) := AcES c 1\ ( v xEM X); 10. output fM(P)

end.

Figure 1: The transformation fM(P)

Definition 3.2 An interpretation I for a program P is unfounded-free iff no nonempty subset of I is an un­ founded set for P w.r.t. I. D

The unfounded-free condition singles out precisely the stable models.

Theorem 3.3 (Theorem 4.6 in [Leone et . al., 1997}) Let M be a model for a program P. M is a stable model for P iff M is unfounded-free.

Example 3.4 Let P = {a V b +-}. M1 = {a} is a stable model of p' since there is no nonempty subset of M1 which is an unfounded set. On the other hand, for M2 = {a, b }, due to Condition 3, both {a} and {b} are unfounded sets. M2 is not unfounded-free, and therefore, it is not a stable model. D

4 From Stable Model Checking to UN SAT

In this section we present a reduction from stable model checking to UNSAT, the complement of Satisfiability, a problem which is better explored in AI and for which efficient algorithms and systems are available.

Recall that a CNF formula over a set A of atomic propositions is a conjunction of the form ¢ = c1 1\ · · · 1\ Cn, where c1 , · · ·, Cn are clauses over A. Without loss of generality, in this paper a clause c = a1 V · · · V am V ·b1 V · · · V ·br will be written as a1 V · · · V am +- b1 1\ · · · 1\ br; thus, a CNF ¢will be a conjunction of these implications.

A formula ¢ is satisfiable if there exists a truth as­ signment to the propositions of A which makes ¢ true; otherwise, ¢ is unsatisfiable (or inconsistent).

UNSAT is the following decision problem.

Given a CNF formula ¢, is it true that ¢ is unsatisfiable?

Our reduction from stable model checking to UNSAT is implemented by the algorithm shown in Figure 1.

In the first step of the algorithm shown in Figure 1, the rule a +- c is deleted. In the second step, ·c is removed from the body of the last rule of P; while the third step removes c from the head of the first rule. Thus, after Step 3, the program becomes {a V b +-; a+- b; b +-a} . Steps 4 to 8 switch the bodies and the heads of the rules, yielding the set of clauses S = { +- a 1\ b; b +- a; a +­ b}. Finally, Step 9 constructs the conjunction of the clauses in S plus the clause a V b +-. Therefore, the output of the algorithm is (+-a 1\ b) 1\ (b +-a) 1\ (a+­ b) 1\(a Vb+-).

Now consider model M2 = {a, c}. Here, the first three steps simplify P to {a V c +-; a +- c.}. Steps 4 to 8 swap the heads and bodies of the rules to get { +- a 1\ c; c +-a}, and Step 9 adds a V c +-. So the outcome for M2 is(+- a 1\ c) 1\ (c +-a) 1\ (a V c +-). D

Theorem 4.2 Given a model M for a ground DLP pro­ gram P, let fM(P) be the CNF formula computed by the algorithm of Figure 1 on input P and M.

Then, M is a stable model for P if and only if rM (P) is unsatisfiable.

In the remainder of this section we demonstrate The­ orem 4.2 (i.e., we show the correctness of our rM(P) reduction). For space limitation, we do not include the proofs of the two lemmas here; but we illustrate their validity on a running example.

To better illustrate the fM (P) transformation, we pro­ ceed in an incremental way, dividing the transformation into three steps, and showing the correctness of each of them.

Definition 4.3 Let P be a ground DLP program and M be a model for P. Define the simplified version aM(P) of P w.r.t M as:

Thus, aM(P) coincides with the program P' obtained by steps 1- 3 of Figure 1. Observe that every rule in aM(P) has a non-empty head. Indeed, if aM(P) would contain a rule r with an empty head, then M would not be a model for P, as the rule of P corresponding to r would have a true body and a false head. Moreover, the simplified program aM(P) is positive (·-free) and it only contains atoms that are true w.r.t . M .

Next, we observe that aM(P) is equivalent toP as far as the stability of M is concerned.

Lemma 4.4 Let P be a DLP program and M be a model for P. Then, M is a stable model for P if and only if it is a stable model for aM (P).

Example 4.5 Take P and the two models M1 and M2 from Example 4.1. M1 is a stable model for P , while M2 is not. Indeed, M1 is a stable model for aM, (P) = {a V b +-; a+- b; b +-a} and M2 is not a stable model for aM 2 (P) ={a V c +-; a+- c}. D

Next, we show that by simply swapping the heads and bodies of the rules of the simplified program aM(P), we get a set of clauses whose models correspond to the un­ founded sets of P w.r.t. M .

Definition 4.6 Let P be a DLP program and M be a model for P . Define f3M (P) as the following set of clauses ·over M:

Observe that f3M(P) coincides with the set of clauses S constructed after steps 1- 8 of Figure 1.

Lemma 4. 7 Let P be a ground DLP program, M be a model for P, and X ~ M. Then X is a model for f3M (P) iff it is an unfounded set for P w. r. t. M .

Example 4.8 f3M 1 (P) is {+-a 1\ b; b +-a; a+- b}, The only subset of M1 which is a model for f3M, (P) is 0. Indeed, 0 is the only unfounded set for P w.r.t. M1 (contained in M1).

f3M 2 (P) is equal to{+- a l\ c; c +-a} . 0 and {c} are the subsets of M2 which are models of f3M 2 (P) . Indeed, they are precisely the unfounded sets for P w.r.t. M2 (contained in M2) . 0

We are now in a position to demonstrate our main theorem.

Proof of Theorem 4.2(Sketch) In the following, we show that fM(P) is unsatisfiable iff Pis unfounded-free; the statement will then follow from Theorem 3.3.

It is easy to see that the output rM(P) of the algo­ rithm of Figure 1 coincides with the conjunction of all clauses in f3M(P) and the clause VxEMX. From Lemma 4.7, the models of f3M(P) are precisely the unfounded sets of P w.r.t. M. Therefore, the models of fM(P) are exactly the non-empty unfounded sets of P w.r.t. M , since every model of rM(P) must satisfy also the clause VxEMX· Thus, M contains no nonempty unfounded set for P (i.e., it is unfounded-free) iff rM(P) has no model (i.e., it is unsatisfiable). 0

Example 4.9 M1 = {a , b} is a stable model for P. Indeed, rM,(P) = (+- a l\ b) 1\ (b +-a) 1\ (a+- b) 1\ (a V b +-) is unsatisfiable.

Differently, M2 = {a, c} is not stable for P. Indeed, r M 2 (P) = (+-a 1\ c) 1\ (c +-a) 1\ (a v c +-) is satisfied by model {c}. 0

The next theorem shows that rM (P) is also an efficient transformation.

Theorem 4.10 Given a model M for a ground DLP program P, let rM(P) be the CNF formula computed by the algorithm of Figure 1 on input P and M. Then, the following holds.

1. fM(P) is logspace computable from P and M.

2. fM(P) is a parsimonious transformation.

3. lfM(P)I :::; IPI + IMI.

Proof (Sketch) fM(P) is the conjunction of the clauses in f3M (P) plus the disjunction of the proposi­ tions in M. The size of f3M(P) is equal to the size of aM(P) , which is smaller than the size of P . Thus, ifM(P)I :::; IPj + IMI.

fM(P) is clearly parsimonious, as it is a formula over the propositions of M only.

Finally, it is easy to see that rM(P) can be computed by a logspace Thring Machine. Indeed, rM (P) can be generated by dealing with one rule of P at a time, with­ out storing any intermediate data apart from a (fixed) number of indices. 0

5 Implementation alild Benchmarks

In order to check the concrete usability of our results, we have implemented our approach to stable model checking in the disjunctive logic programming system dl v [Eiter et. al., 1997b; 1998].

dl v is a knowledge representation system which has been developed at Technische Universitat Wien. Re­ cent comparisons [Eiter et. al., 1998] have shown that dl vis nowadays a state-of-the-art implementation of dis­ junctive logic programming. To our knowledge, dl v is the only publicly available system which supports full (function-free) disjunctive logic programming under sta­ ble model semantics.

The computational engine of dl v implements the theo­ retical results achieved in [Leone et. al., 1997]. Roughly, the system consists of two main modules: the Model Generator (MG) and the Model Checker (MC). MG pro­ duces stable model candidates, whose stability is then checked by the MC.

We have replaced the Model Checker of dl v by new modules implementing the results of the previous sec­ tion, running some benchmark problems and comparing the execution times.

Overview of the Compared Methods

We have compared the following methods for stable model checking (the labels below are used in Figures 2, 3, and 4).

· (Old Checker.) The old model checker of the dlv system [Leone et. al., 1997; Eiter et. al., 1997b]. Its strong points are the efficient evaluation of head cycle free (HCF) programs [Ben-Eliyahu and Dechter, 1994] and the use of modular evaluation techniques. Indeed, HCF programs are evaluated in polynomial time and, if the program is not HCF, the inefficient part of the com­ putation is limited only to the subprograms 1 which are not HCF (while the polynomial time algorithm is applied to the HCF subprograms). Polynomial space and single exponential time bounds are always guaranteed.

· (fM+DP.) Given a program P and a model M to be checked for stability, an implementation of the algorithm of Figure 1 generates the CNF formula fM(P), which is then submitted to a Satisfiability checker. If the Satisfi­ ability checker returns true (fM(P) is satisfiable), then M is not a stable model of P; otherwise (rM (P) is un­ satisfiable), M is a stable model of P. For checking Satisfiability of rM(P) , we have used an efficient imple­ mentation of the Davis-Putnam procedure called SATO [Zhang, 1997].

1 A subprogram of P is the set of rules defining the atoms of the same strongly connected component of the dependency graph of P [Leone et. al., 1997] .

· (fM+DP+Mod.) This is an improved version of the method above, enhanced by modular evaluation tech­ niques derived from the combination of Lemma 4.4 with the modularity results of [Leone et. al., 1997]. Roughly, given P and M, Pis first simplified (steps 1- 3 of Figure 1) computing the program aM(P). The subprograms of aM(P) are then evaluated one-at-a-time. A polynomial time method is applied to HCF subprograms (as in Old Checker) ; while the fM+DP method is applied to non­ HCF subprograms.

Benchmark Problem

In order to generate some co-NP-hard model checking in­ stances, which could better highlight the differences be­ tween the model checking techniques, we needed to run ~f -hard problems on the DLP system at hand. Thus, we have compared the performance of the different model checking methods by running various instances of the ~f -complete problem Strategic Companies on the dl v system.

The strategic companies problem is from [Cadoli et. al. , 1997]; it is, to the best of our knowledge, the only ~f -complete KR problem from the business domain. No experimental results for any ~f -complete KR problems are known.

Briefly, a holding owns companies, each of which pro­ duces some goods. Moreover, several companies may have joint control over another company. Now, some companies should be sold, under the constraint that all goods can be still produced, and that no company is sold which would still be controlled by the holding after the transaction. A company is strategic, if it belongs to a strategic set, which is a minimal set of companies satis­ fying these constraints. Those sets are expressed by the following natural program:

strategic (Cl) V strategic (C2) ~ produced_by (P, Cl, C2). strategic (C) ~ controlled_by (C, Cl, C2, C3) 1\ strategic(Cl) 1\ strategic(C2) 1\ strategic (C3).

Here strategic( C) means that C is strategic, produced_by(P, C1, C2) that product P is produced by companies C1 and C2, and controlled_by(C, C1 , C2, C3) that C is jointly controlled by C1, C2 and C3; we have adopted here from [Cadoli et. al., 1997] that each product is produced by at most two companies and each company is under joint control of at most three other companies.

The problem is to find out the set of all strategic com­ panies (i.e., under brave reasoning, for which C the fact strategic(C) is true).

Note that this problem cannot be expressed by a fixed normal (V-free) logic program uniformly on all collections of facts produced_by(p, cl, c2) and controlled_by(c, cl , c2,c3) (unless NP = ~f, an un­ likely event). Thus, Strategic Companies is an example of a relevant problem where the expressive power of dis­ junctive logic programming is really needed.

Benchmark Data

We have generated tests with instances for n companies and 3n products.

We have uniform randomly chosen the produced_by and the controlled_by relations , where each company is controlled by one to five companies (Obeying the obvi­ ous constraints that no company can control itself, and that two consortia have to have at least one member in common). On average there are 1.5 controlled_by relationships per company.

Discussion of Results

Our experiments were run on a 133 MHz i486-compatible PC under Linux, using egcs-2.91.14 C++ compiler.

The results are displayed in the graphs of Figures 2- 4. Execution times are reported on the vertical axis, while the horizontal axis displays the size of the problem in­ stance (number of companies of the instance of Strategic Companies to be solved). We have run instances of a size increasing a step of 5 companies, up to 100 companies.

The graph of Figure 2 shows the total time employed by the (stable) Model Checkers for the computation of all stable models of the program (i.e., for the generation of all sets of strategic companies). Note that a program having n stable models requires m ~ n calls to the Model Checker (m- n is the number of calls on models which are not stable); the sum of the times employed for check­ ing the stability of all m models is displayed in the graph. For each problem size (number of companies) x, we have run 25 instances of size x and reported the average time. Thus, this graph shows the practical impact of the vari­ ous model checking strategies on the computation.

f M+DP clearly outperforms Old Checker: the time employed by r M+DP to solve an instance of 100 com­ panies is not sufficient for Old Checker even to solve instances of 25 companies. Interestingly, modular eval­ uation techniques appear very useful: f M +DP+Mod takes less than 5% off M+DP to solve problems of size 100.

The graph in Figure 3 refers to the same runs of the previous graph; but it shows the longest times required by each method for checking the stability of a single model. This time, the curves are not very regular, be­ cause they visualize times of single calls (rather than average times as in Figure 2) of randomly generated instances. Also in this graph the new strategies show better performances than the old dlv checker. Surpris­ ingly, the difference between the times of f M+DP and l'M+DP+Mod is much smaller than in the previous graph. We have the following explanation for this phenomenon. Modular evaluation techniques speed up the computa­ tion of most instances. (Thus, modularity significantly affects total model checking time.) However, very hard instances cannot be "decomposed" by modular evalua­ tion techniques. (Thus, the worst case times for single calls to the model checker are similar.)

Finally, the graph in Figure 4 refers to the computa­ tion of one stable model (i.e., to the computation of one set of strateffiic companies - sufficient to solve the corre­ sponding ~2 decision problem). It compares the over­ all execution time (model generation + model checking time) taken by the dlv system when the (old) model checker is replaced by our new model checkers. The ad­ vantage of using fM+DP+Mod is very evident: by using f M+DP+Mod an instance of size 100 is solved more quickly· than an instance of size 20 with the old system. This graph also shows the time taken by dl v for model gen­ eration alone. Most of the execution time needed for computing one stable model is consumed for the genera­ tion of the models; only a very low percentage of the time is consumed by the Model Checker r M+DP+Mod itself.

In conclusion, observe that we have also compared the model checking strategies on a number of problems "eas­ ier" than Stategic Companies (at most NP-complete) ; as expected, the methods behaved very similarly.