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.

** (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).

** (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.

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.

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.

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.

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.

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.