Tractable Cover Compilations

1 Introduction

Different approaches have been proposed to circumvent the intractability of propositional deduction. Some of them restrict the expressive power of the representa­ tion language to tractable classes, like the Horn, re­ verse Horn, binary, monotone, renamable Horn, q-Horn, nested clauses formulas [Dowling and Gallier, 1984; Lewis, 1978; Boros et al. , 1994; Knuth, 1990). Unfortu­ nately, such classes are not expressive enough for many applications. Contrastingly, compilation approaches ap­ ply to full propositional-logic knowledge bases (KBs for short). Thanks to an off-line pre-processing step, a KB ~ is compiled into a formula ~· so that on-line query answering can be performed tractably from ~· . Many approaches to compilation have been proposed so far, mainly [Reiter and De Kleer, 1987; Selman and Kautz, 1991; 1994; del Val, 1994; Dechter and Rish, 1994; Marquis, 1995; del Val, 1995; 1996; Marquis and Sa­ daoui, 1996; Schrag, 1996).

*This work has been supported in part by the Ganymede II project of the Contrat Etat/Region Nord- Pas-de-Calais.

2 CRIL 3 IUT de Lens Universite d'Artois Rue de l'Universite, S.P. 16 F-62307 Lens Cedex, FRANCE

{gregoire,marquis,mazure,sais }@cril.univ-artois.fr

In this paper, a new approach to equivalence-pre­ serving compilation, called tractable covers, is intro­ duced. In short, a tractable cover of ~ is a finite set T of tractable formulas <P (disjunctively considered) s.t. ~ = T Tractable covers of ~ are equivalence-preserving compilations of~: a clause c is a logical consequence of ~ iff for every <P in T, c is a logical consequence of <P. Since <P is tractable, each elementary test <P f= c can be computed in time polynomial in I<PI + 14 The point is to find out tractable <Ps that concisely represent (i.e. cover) the largest sets of models of ~, so that I Tl remains limited. To some extent, the present work could then be related to other model-based approaches to knowledge representation and reasoning, like [Khardon and Roth, 1996).

First, a general framework is presented, which can take advantage of most tractable classes, simultaneously. In many respects, it generalizes the prime implicants cover technique recently used for compilation purpose [Schrag, 1996). Then, the focus is laid on tractable covers that can be computed and intensionally represented thanks to (partial) interpretations. Two specific cases are consid­ ered. In the first one, partial interpretations are used to shape the KB into formulas from several possible classes. In the second one, they are used to derive renam­ able Horn formulas . The last one is proved less space­ consuming than prime implicants covers [Schrag, 1996) for every KB. Since tractable covers of~ are equivalence­ preserving compilations, their size may remain exponen­ tial in 1~1 unless NP ~ Pfpoly [Selman and Kautz, 1994), which is very unlikely. However, experimental re­ sults show that the new approaches can prove efficient w.r.t. direct query answering and offer significant time and space savings w.r.t. prime implicants covers.

2 Formal Preliminaries

A literal is a propositional variable or a negated one. A clause (resp. a term) is a finite set of literals, represent­ ing their disjunction (resp. conjunction). A Horn (resp. reverse Horn) clause contains at most one literal that is positive (resp. negative) . A binary clause contains at most two literals. A KB 'E is a finite set of propositional formulas, conjunctively considered. Var('E) is the set of variables occurring in 'E. Every KB can be rewritten into a conjunction of clauses (into CNF for short) while preserving equivalence. A KB 'E is said renamable Horn iff there exists a substitution u over literals l built up from Var('E), s.t. u(l) = [and u('E) is Horn.

Interpretations and models are defined in the usual way. Let us stress that, quite unconventionally, (partial) interpretations will be represented as terms, i.e. as satis­ fiable sets of literals (vs. sets of variables) . An implicant of a KB 'E is a partial interpretation a s.t. a f= 'E. A prime implicant of 'E is an implicant 1r of 'E s.t . for all implicants a of 'E s.t . 1r f= a, we have a f= 1r. The set of all prime implicants of 'E (up to logical equivalence) is noted PI('E). A prime implicant cover of 'E is any subset S of PI('E) (disjunctively considered) s.t. S ='E.

3 Tractable Cover Compilations

3.1 The General Framework

First, let us make precise what classes of tractable for­ mulas will be considered:

Definition 3.1 A list C s of classes C of tractable propo­ sitional formulas (w.r.t . cover compilation} is s.t.:

• There exists a polytime algorithm TRACT ABLE? for checking whether any formula <I> belongs to C .
• There exists a polytime algorithm QUERY? for checking whether <I> ~ c holds for any <I> in C and any clause c.
• For every C in Cs, for every formula <I> of C and every term p, there exists C' in Cs s. t. (<I> 1\ p) E C' .

Since classes of tractable formulas are not fini­ te sets in the general case, they are intensionally represented by ordered pairs of decision procedures (TRACT ABLE?, QUERY?) . .

Interestingly, the great majority of classes of formu­ las tractable for SAT (the well-known propositional sat­ isfiability decision problem) are also tractable for cover compilations. Especially, this is the case for the Horn, re­ verse Horn, binary, renamable Horn, q-Horn and nested clauses classes.

We are now ready to define the notion of a tractable cover of a propositional KB.

Definition 3.2 Given a CNF-KB ~ and a finite list Cs of classes of tractable formulas w. r. t. cover compilation {repre­ sented intensionally}, a tractable cover of~ w.r.t. Cs is a finite set T of satisfiable formulas (disjunctively considered) s.t.:

• For every <l>; E T , there exists C in Cs s.t. <I>; belongs to C, and
• T= ~.

In the following, we will assume that C s contains at least the class { t s. t. t is a term} . This ensures that there always exists at least one tractable cover of 'E, namely a prime implicants one.

In this paper, we focus on tractable covers that can be intensionally represented, using (partial) interpretations. The corresponding explicit covers can be generated on­ line from the intensional ones in polynomial time.

3.2 Carver-Based Tractable Covers

A first way to derive covers consists in simplifying the KB using partial interpretations. For any partial inter­ pretation p = {l1 , ... , ln}, the KB 'E simplified w.r.t. p is the set 'Ev = ((('Et 1 )t 2 ) · ·· )1.., where 'Et = {c\ {...,z} s.t . c E 'E and c n {l} = 0}.

Definition 3.3 Given a CNF-KB ~ and a finite list Cs of classes of tractable formulas (represented intensionally}:

• A carver of~ w. r. t . C s is a partial interpretation p s. t. there exists C in Cs s.t. ~P belongs to C and ~P is satisfiable.
• A carver-based tractable cover of~ w.r.t. Cs is a set PC of carvers of~ w. r. t. C s (disjunctively considered} s.t. (PC 1\ ~) :::: ~.
• A carver-based cover compilation of~ is a pair C = (~,PC) , where PC is a carver-based tractable cover of ~ w.r.t. Cs .

Interestingly, the space required to store a carver p is always lower or equal to the space needed by the corre­ sponding tractable formula <I> = p 1\ 'Ev (with a O(I'EI) factor in the worst case). At the on-line query answering stage, the price to be paid is a O(I'E /\pi) time complex­ ity overhead per carver p but this does not question the tractability of query answering.

As an example, let 'E = {x1 Vx2 Vx3 Vx4,x1 Vx2 Vx4} and let C s contain the Horn and the binary classes. The set PC= {{xi}, {xi}} is a carver-based tractable cover of 'E w.r.t. Cs since 'E{xt} = {x2 V X3 V x4} is Horn and 'E{:ft} = {x2 V x4} is binary. If Cs reduces to the renamable Horn class, {0} is a carver-based tractable cover of 'E w.r.t. Cs since 'E belongs to the renamable Horn class.

Clearly enough, carver-based cover compilations are equivalence-preserving compilations:

Proposition 3.1 Let ~ be a CNF-KB, C = (~,PC) be a carver-based cover compilation of ~ and let c be a clause. ~ ~ c iff for every p in PC, ((p ~ c) or (~p ~ c)) , which can be decided in time polynomial in ICI + lei.

Although the class(es) to which 'Ep belongs can be polynomially recognized on-line for each carver p of PC, in practice, they are determined once only at the off-line compiling stage. Accordingly, each carver p found during the compiling process is indexed with a reference label(p) to the concerned class in Cs . A significant amount of time in on-line query answering can be saved via such indexing.

Interestingly, carver-based cover compilations can lead to exponential space savings w.r.t . prime implicants cover compilations for some KBs. An extreme case con­ sists of tractable KBs I: that remain invariant under carver-based cover compilation but are such that every prime implicant cover is exponential in the size of I:.

3.3 Hyper-Implicant Covers

Formulas in covers must be tractable and exhibit as many models of I: as possible. Interestingly, several classes C of tractable formulas admit model-theoretic characterizations and features that can be exploited. For the binary, Horn, reverse Horn, renamable Horn classes, among others, class membership is equivalent to the ex­ istence of some specific interpretation(s). Formally, a CNF-KB I: is renamable Horn [Lewis, 1978] iff there ex­ ists an interpretation p over Var(I:) s.t. for every clause c of I:, at most one literal of c does not belong top. In­ terestingly, the renamable Horn class includes both the Horn, reverse Horn, and satisfiable binary KBs as proper subsets.

As the semantical characterizations above indicate it, literals that belong both to p and to I: play a central role that we can take advantage of. In order to derive satisfiable renamable Horn formulas, every clause c of I: is shortened using a model p = m of I:: only the literals occurring in m are kept, plus an additional literal of c (when possible). In this way, every shortened clause is such that every literal of m (except possibly one) belongs to it. Accordingly, the resulting set of clauses, called hyper-implicant of I:, is satisfiable and renamable Horn.

Formally, let m be a model of I:. For every clause c in I:, let em be the clause consisting of the literals common to c and m. Let P(I:, m) denote the set of clauses of I: s.t. for every clause c in P(I:, m), c and em are identical. Let N(I:, m) be I: \ P(I:, m). For every clause c in N(I:, m), let l~ denote a literal ofc s.t. l~ belongs tom. Obviously, several candidates l~ may exist in the general case.

Definition 3.4 Given a CNF-KB I;;

• A hyper-implicant of I; (w.r.t. to a model} m of I; is a formula I:m = ( 1\ c)!\ ( 1\ (em V l~)). cEP(E,m) cEN(E,m)
• A hyper-implicant cover 1i of I; is a set of hyper­ implicants of I; (disjunctively considered} s. t. 1i = I; .

Importantly, the size of any hyper-implicant I:m of I: is strictly lower than the size of I:, except when I: is renamable Horn.

Hyper-implicant covers are equivalence-preserving compilations:

Proposition 3.2 Let I; be a CNF-KB, 1i be a hyper­ implicant cover of I; and c be a clause. I; f= c iff for ev­ ery hyper-implicant I;m of 1i, we have I;m f= c. This can be decided in time linear in !HI + !c!.

Assuming that the clauses in I: = { c1 , ... , Cn} are to­ tally ordered, hyper-implicant covers can be represented intensionally by I: and sets of pairs (m, [l~, . . . , l~]) where m is a model of I: and l~ (i E l..n) is false if ci E P(I:, m) and is the literal of Ci \ m which is kept, otherwise. Each I:m can be derived on-line from I: and (m, [l~, ... , l~]) in linear time.

As an example, let I: = { x1 V X3 V X4, x1 V x2 V X3, X1 V X2 V fE3 V X4, X1 V X2 V X3 V X4, X1 V X2 V X3 V x4 }. The hyper implicant cover represented by I: and the two pairs ({xl,x2,x3,x4},[x3,x3,x2,xl,xl]) and ( {x1, x2, x3, x4}, [x1, x2, x3, x2, x4]), contains two hyper­ implicants: { X1 V X4 V X3, X1 V X2 V X3, X1 V X3 V X2, X2 V x3 V x1,x3 V x4 V xi} and {x3 V X1,X3 V X2,X2 V X4 V X3,Xl v X4 v X2,Xl v X2 v X4}·

Intuitively, any hyper-implicant I:m of I: is a concise representation of some prime implicants of I:. To be more specific, the prime implicants of I: which are en­ tailed by m are prime implicants of I:m.

Proposition 3.3 For every model m of I;, let P Im (I;) be the set of prime implicants of I; s.t. for every 1r in Plm(I;) , we have m f= 1r. Then, Plm(I;) ~ PI(I;m).

Consequently, I:m covers every model of I: covered by a prime implicant of I: entailed by m.

Hyper-implicants covers are economical representa­ tions w.r.t. prime implicants ones. Not withstanding the fact that hyper-implicants of I: are smaller than I:, the number of hyper-implicants in a cover is lower than the number of implicants in a cover:

Proposition 3.4 For every prime implicant cover of I; con­ taining t prime implicants there exists a hyper-implicant cover . lt + lJ h . r t of I; containmg at most - 2 - yper-~mp ~can s.

In the example above, the hyper-implicant cover con­ tains 2 formulas, while the smallest prime implicant cover of I: consists of 6 prime implicants. Actually, ex­ periments show significant savings w.r.t. the sizes of the prime implicants covers for most KBs (cf. Section 5).

4 Computing Compilations

(Partial) interpretations giving rise to intensionally­ represented tractable covers are computed using system­ atic search, thanks to a Davis/Putnam-like procedure DPTC. This procedure is closely related to Schrag's DPPI algorithm [Schrag, 1996]. Cs is empty for the hyper­ implicant case.

DPTC(I:,Cs):

• 1 PC f- 0; 2 DP*(I:,Cs,0); 3 Return ((I:, PC)) .

DP*(I:,Cs,p):

• 1 If not PRUNING(I:,p) then
• 2 UNIT_PROPAGATE(I:,p);
• 3 If 0 E I: then return;
• 4 If (p t= I:)

5 6 7 8 9 then PROCESS_IMPLICANT(p,~,Cs) return; lt- CHOOSE_BEST_LITERAL(~); DP·(~,Cs,pU {l}); DP*(~, Cs,pU {·l}).

The CHOOSE...BESLLITERAL branching rule and UN­ ILPROPAGATE procedures are standard Davis/Putnam features. In our experiments, the branching rule by [Du­ bois et al., 1996) is used. The main role of DP* is to find implicants of ~ in the whole search tree. PRUNING and PROCESS_!MPLICANT depend on the considered ap­ proach. From the found implicants, (partial) interpre­ tations (carvers and implicit representations of hyper­ implicants) are derived thanks to PROCESS_IMPLICANT; they are collected into the global variable PC.

4.1 The Carver-Based Case

PRUNIN�c (~,new_p): 1 If there exists p E PC s. t. (new_p F p) 2 then return(true) else return(false). PROCESS_IMPLICANTc(new_p,~,Cs): 1 Carver t- DERIVEc(new_p,~,Cs); 2 For every p E PC do 3 If (pF Carver) then remove p from PC; 4 Put Carver in PC. DERIVEc (p,~,Cs): 1 Prime t- ONE_PRIME(p,~); 2 For every literal l E Prime do 3 For every (TRACTABLE?,QUERY?) in Cs do · 4 If TRACT ABLE?(~Prime\{l}) then Return(DERIVEc (Prime\{l} , ~,Cs)); 5 Return(Prime).

Whenever an implicant p of ~ is found, a prime im­ plicant Prime of ~ s.t. p F Prime is extracted from p, thanks to the ONE_FRIME procedure. ONE.JlRIME consid­ ers every liter all of p successively, check whether l is nec­ essary (i.e. if there exists a clause c of~ s.t. cnp = { l} ), and remove l from p if lis not necessary (see [Castell and Cayrol, 1996][Schrag, 1996) for details). These prime im­ plicants are then tentatively simplified; all the literals of each Prime are considered successively; for every literal l of Prime, ~Prime\{! } is checked for tractability using the recognition procedures given in Cs. If ~Prime\{!} is found tractable, l is ruled out from Prime and is kept otherwise. Once all the literals of Prime have been con­ sidered, the resulting simplified Prime (indexed by the label of the corresponding class in Cs) is checked against the set PC of carvers collected so far . Only maximal carvers w.r.t. F are kept in PC. Interestingly, the set PC of carvers stored during the traversal of the DP search tree is used to prune this tree, thanks to the PRUNINGc procedure; indeed, whenever a candidate (partial) interpretation new_p is elected, it can be immediately re­ moved if new_p entails one of the current carvers.

Clearly enough, both the literal ordering and the recognition procedure ordering used in DERIVEc can greatly influence the cover generated in this way.

4.2 The Hyper-Implicant Case

PRUNIN�s(~,new_p): 1 If there exists p E PC s. t. (~new_p F ~P) 2 then return(true) else return(false). PROCESS_IMPLICANTs(new_p,~,_): 1 Model t- DERIVEs(new_p,~); 2 For every p E PC do 3 If (~Model F ~P) then remove p from PC; 4 Put Model in PC. DERIVEs (p, ~) : 1 Model t- p; 2 For every variable v E V ar(~) do 3 If ({v}np=0) and ({·v}np=0) 4 then put v with its most frequent sign in ~ to Model; 5 Return(Model).

Each time an implicant p of ~ is found , a model Model of ~ s.t. Model F p is derived from p. The vari­ ables that do not occur in p are added with the sign occurring the most frequently in ~- When ~Model is computed for the first time, a list [l~ , ... , l'::,] is at­ tached to Model. The DERIVEs procedure is both sim­ pler and more efficient than DERIVEc (roughly, it is not more time-consuming than the prime implicant extrac­ tion achieved by ONE.JlRIME). The tractable formulas ~P corresponding to the models p collected in PC are used to prune the search tree (PRUNINGs). Only the ps giving rise to the logically weakests ~P are kept in PC. Since the renamable Horn formulas ~Model and ~P stem from the same KB ~ . checking whether (~Model f= ~P) can be performed in a very efficient way.

Both the literals chosen to extend the found impli­ cants to models p of ~. and the literals l'Z' selected in clauses of ~P may have a significant impact on the hyper­ implicants ~P that are generated.

5 Experimental Results

In contrast to SAT, only few benchmarks for knowl­ edge compilation can be found in the literature (with the well-developed experimental framework of [Schrag, 1996) as an exception). Actually, no comprehensive anal­ ysis of what should be the nature of meaningful bench­ marks for evaluating compilation approaches h?S ever been conducted. Clearly, benchmarks must be hard for . query answering since the goal of knowledge compilation is to overcome its intractability. However, in contrast to [Schrag, 1996), we do not focus on hard SAT instances, only. Hard SAT instances (with respect to current algo­ rithms) should be considered hard for query answering since at least one query (namely, the empty clause) is difficult. However, easy SAT instances can exhibit hard queries that differ from the empty clause.

Accordingly, we tested the tractable covers and the prime implicants approaches w.r.t. many KBs, including "standard" structured problems, taken from [Forbus and De Kleer, 1993], and random k-SAT problems [Dubois et al., 1996], varying the #cla(use)f#var(iable) ratio from the easy to the hard regions. Each KB ~ has been compiled using the 3 techniques. Then, 500 queries have been considered. In order to check the usefulness of the compilation process, we also answered these queries from ~' using a direct, uncompiled, Davis/Putnam-based ap­ proach [Dubois et al., 1996]. For each problem ~ and each compilation technique, the ratios a= Qc/Qu and /3 = Cj(Qu- Qc) have been computed. Qc (resp. Qu) is the time needed by the compiled (resp. uncompiled) approach to answer all the queries, and C is the compi­ lation time. a (resp. /3) tells us how much query time improvement we get from compilation (resp. how many queries are required to amortize the cost of compilation).

Table 1 reports some results of our extensive experi­ ments. For each problem [Forbus and De Kleer, 1993], it lists results for the prime implicants, carvers, and hyper­ implicants covers, successively. Especially, it gives the ratios a and /3 and the size (in literals) of the corre­ sponding cover. The size of any tractable cover compi­ lation is the size of ~ plus the size of the set of (partial) interpretations used as an implicit representation. For the carver-based approach, only the Horn, reverse Horn and binary classes have been considered. For the hyper­ implicant approach, simplification of the cover (i.e. lines 2 to 4 of the PROCESS_IMPLICANT'H. procedure) has not been implemented.

Results obtained on 50 variables random 3-SAT prob­ lems, where the ratio #cla/#var varies from 3.2 to 4.4, are reported on the two next figures. 50 problems have been considered per point and the corresponding scores averaged. Figure 1 (resp. Figure 2) gives aggregate val­ ues of ratios a (resp. sizes in literals) obtained for each compilation technique. a = 1 separates the region for which compilation is useful from the region for which it is not.

At the light of our experiments, tractable covers prove better than prime implicants covers, both for structured and random k-SAT problems. Significant time savings w.r.t. query answering and significant space savings are obtained. Especially, tractable covers prove useful for many KBs for which prime implicants covers are too large to offer improvements w.r.t. query answer­ ing. More, the tractable cover approach allows the com­ pilation of KBs which have so huge prime implicants covers P that P cannot be computed and stored. This coheres with the theoretical results reported in [Bouf­ khad and Dubois, 1996], showing that the average num­ ber of prime implicants of k-SAT formulas is exponential in their number of variables.

6 Conclusion

Both theoretical and experimental results show the tractable cover approach promising and encourage us to extend it in several directions. A first issue for further research is how to determine efficiently the best suited classes of tractable formulas for a given KB 1:. On the experimental side, an extensive evaluation of the carver­ based technique equipped with more expressive tractable classes must be done. Extending the hyper-implicant ap­ proach to other tractable classes, especially the q-Horn one [Boros et al., 1994], is another interesting perspec­ tive. Finally, fragments of tractable covers of I: can serve as approximate compilations (lower bounds) of I: in the sense of [Selman and Kautz, 1991; 1994; del Val, 1995; 1996]. Since the tractable cover approach allows disjunc­ tions of tractable formulas from several classes, better approximations could be obtained.