Next: Applications Up: Space Efficiency of Propositional Previous: Reductions among KR Formalisms

# Comparing the Space Efficiency of PKR Formalisms

In this section we show how to use the compilability classes defined in Section 3 to compare the succinctness of PKR formalisms.

Let and be two formalisms representing sets of models. We prove that any knowledge base in can be reduced, via a poly-size reduction, to a knowledge base in satisfying model-preservation if and only if the compilability class of the problem of model checking (first input: KB, second input: interpretation) in is higher than or equal to the compilability class of the problem of model checking in .

Similarly, we prove that theorem-preserving poly-size reductions exist if and only if the compilability class of the problem of inference (first input: KB, second input: formula, cf. definition of the problem PLI) in is higher than or equal to the compilability class of the problem of inference in .

In order to simplify the presentation and proof of the theorems we introduce some definitions.

Definition 10

(Model hardness/completeness) Let be a PKR formalism and C be a complexity class. If the problem of model checking for belongs to the compilability class C, where the model is the varying part of the instances, we say that is in model-C. Similarly, if model checking is C-complete (hard), we say that is model-C-complete (hard).

Definition 11

(Theorem hardness/completeness) Let be a PKR formalism and C be a complexity class. If the problem of inference for the formalism belongs to the compilability class C, whenever the formula is the varying part of the instance, we say that is in thm-C. Similarly, if inference is C-complete (hard), we say that is thm-C-complete (hard).

These definitions implicitly define two hierarchies, which parallel the polynomial hierarchy [49]: the model hierarchy ( model-P, model-NP, model-,etc.) and the theorem hierarchy ( thm-P, thm-NP, thm-,etc.). The higher a formalism is in the model hierarchy, the more its efficiency in representing models is -- and analogously for theorems. As an example [10, Thm. 6], we characterize model and theorem classes of Propositional Logic.

Theorem 3

PL is in model-P and it is thm-coNP-complete.

We can now formally establish the connection between succinctness of representations and compilability classes. In the following theorems, the complexity classes C, C, C belong to the polynomial hierarchy [49]. In Theorems 5 and 7 we assume that the polynomial hierarchy does not collapse.

We start by showing that the existence of model-preserving reductions from a formalism to another one can be easily obtained if their levels in the model hierarchy satisfy a simple condition.

Theorem 4

Let and be two PKR formalisms. If is in model-C and is model-C-hard, then there exists a poly-size reduction satisfying model preservation.

Proof. Recall that since is in model-C, model checking in is in C, and since is model-C-hard, model checking in is non-uniformly comp-reducible to model checking in . That is, (adapting Def. 6) there exist two poly-size binary functions and , and a polynomial-time binary function such that for every pair it holds that

(note that is the poly-time function appearing in Def. 6, different from which is the poly-size circuit appearing in Def. 8).

Now observe that can be computed from by simply counting the letters appearing in ; let be such a counting function, i.e., . Clearly, is poly-size. Define the reduction as . Since poly-size functions are closed under composition, is poly-size. Now we show that is a model-preserving reduction. By Definition 8, we need to prove that there exists a polynomial such that for each knowledge base in , there exists a poly-size circuit such that for every interpretation of the variables of it holds that iff .

We proceed as follows: Given a in , we compute . Since and are poly-size, has size polynomial with respect to . Define the circuit as the one computing . Since is a poly-time function over both inputs, and is poly-size in , there exists a representation of as a circuit whose size is polynomial wrt . From this construction, iff . Hence, the thesis follows.

The following theorem, instead, gives a simple method to prove that there is no model-preserving reduction from one formalism to another one.

Theorem 5

Let and be two PKR formalisms. If the polynomial hierarchy does not collapse, is model-C-hard, is in model-C, and C C, then there is no poly-size reduction satisfying model preservation.

Proof. We show that if such a reduction exists, then C/poly C/poly which implies that the polynomial hierarchy collapses at some level [52]. Let be a complete problem for class C -- e.g., if C is then may be validity of -quantified boolean formulae [49]. Define the problem as follows.

We already proved [6, Thm. 6] that is C-complete. Since model checking in is model-C-hard, is non-uniformly comp-reducible to model checking in . That is, (adapting Def. 6) there exist two poly-size binary functions and , and a polynomial-time binary function such that for every pair , it holds if and only if . Let . Clearly, the knowledge base depends only on , i.e., there is exactly one knowledge base for each integer. Call it . Moreover, also depends on only: call it (for Oracle). Observe that both and have polynomial size with respect to .

If there exists a poly-size reduction satisfying model preservation, then given the knowledge base there exists a poly-size circuit such that if and only if .

Therefore, the C-complete problem can be non-uniformly reduced to a problem in C as follows: Given , from its size one obtains (with a preprocessing) and . Then one checks whether the interpretation (computable in polynomial time given , and ) is a model in for . From the fact that model checking in is in C, we have that C C. We proved in a previous paper that such result implies that C/poly C/poly [6, Thm. 9], which in turns implies that the polynomial hierarchy collapses [52].

The above theorems show that the hierarchy of classes model-C exactly characterizes the space efficiency of a formalism in representing sets of models. In fact, two formalisms at the same level in the model hierarchy can be reduced into each other via a poly-size reduction (Theorem 4), while there is no poly-size reduction from a formalism () higher up in the hierarchy into one () in a lower class (Theorem 5). In the latter case we say that is more space-efficient than .

Analogous results (with similar proofs) hold for poly-size reductions preserving theorems. Namely, the next theorem shows how to infer the existence of theorem-preserving reductions, while the other one gives a way to prove that there is no theorem-preserving reduction from one formalism to another one.

Theorem 6

Let and be two PKR formalisms. If is in thm-C and is thm-C-hard, then there exists a poly-size reduction satisfying theorem preservation.

Proof. Recall that since is in thm-C, inference in is in C, and since is thm-C-hard, inference in is non-uniformly comp-reducible to inference in . That is, (adapting Def. 6) there exist two poly-size binary functions and , and a polynomial-time binary function such that for every pair it holds that

(here we distinguish the poly-time function appearing in Def. 6 and the poly-size circuit appearing in Def. 9).

Using Theorem 1 we can replace with an upper bound in the above formula. From Assumption 1, we know that the size of is less than or equal to the size of ; therefore we replace with . The above formula now becomes

Define the reduction as , where is the poly-size function that computes the size of its input. Since poly-size functions are closed under composition, is poly-size.

Now, we show that is a theorem-preserving reduction, i.e., satisfies Def. 9. This amounts to proving that for each knowledge base in there exists a circuit , whose size is poynomial wrt , such that for every formula on the variables of it holds that iff .

We proceed as in the proof of Theorem 4: Given a in , let . Since and are poly-size, has polynomial size with respect to . Define . Clearly, can be represented by a circuit of polynomial size wrt . From this construction, iff . Hence, the claim follows.

Theorem 7

Let and be two PKR formalisms. If the polynomial hierarchy does not collapse, is thm-C-hard, is in thm-C, and C C, then there is no poly-size reduction satisfying theorem preservation.

Proof. We show that if such a reduction exists, then C/poly C/poly and the polynomial hierarchy collapses at some level [52]. Let be a complete problem for class C. Define the problem as in the proof of Theorem 5: this problem is C-complete [6, Thm. 6]. Since inference in is thm-C-hard, is non-uniformly comp-reducible to inference in . That is, (adapting Def. 6) there exist two poly-size binary functions and , and a polynomial-time binary function such that for every pair , if and only if . Let . Clearly, the knowledge base depends just on , i.e., there is one knowledge base for each integer. Call it . Moreover, also depends just on : call it (for Oracle). Observe that both and have polynomial size with respect to .

If there exists a poly-size reduction satisfying theorem preservation, then given the knowledge base there exists a poly-time function such that if and only if .

Therefore, the C-complete problem can be non-uniformly reduced to a problem in C as follows: Given , from its size one obtains (with an arbitrary preprocessing) and . Then one checks whether the formula (computable in poly-time given and ) is a theorem in of . From the fact that inference in is in C, we have that C C. It follows that C/poly C/poly [6, Thm. 9], which implies that the polynomial hierarchy collapses [52].

Theorems 4-7 show that compilability classes characterize very precisely the relative capability of PKR formalisms to represent sets of models or sets of theorems. For example, as a consequence of Theorems 3 and 7 there is no poly-size reduction from PL to the syntactic restriction of PL allowing only Horn clauses that preserves the theorems, unless the polynomial hierarchy collapses. Kautz and Selman [30] proved non-existence of such a reduction for a problem strictly related to PLI using a specific proof.

Next: Applications Up: Space Efficiency of Propositional Previous: Reductions among KR Formalisms
Paolo Liberatore
2000-07-28