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 $F_1$ and $F_2$ be two formalisms representing sets of models. We prove that any knowledge base $\alpha$ in $F_1$ can be reduced, via a poly-size reduction, to a knowledge base $\beta$ in $F_2$ satisfying model-preservation if and only if the compilability class of the problem of model checking (first input: KB, second input: interpretation) in $F_2$ is higher than or equal to the compilability class of the problem of model checking in $F_1$.

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 $F_1$ is higher than or equal to the compilability class of the problem of inference in $F_2$.

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

Definition 10  

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

Definition 11  

(Theorem hardness/completeness) Let $F$ be a PKR formalism and C be a complexity class. If the problem of inference for the formalism $F$ belongs to the compilability class $\parallel\!\leadsto$ C, whenever the formula is the varying part of the instance, we say that $F$ is in thm-C. Similarly, if inference is $\parallel\!\leadsto$ C-complete (hard), we say that $F$ 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-$\Sigma^p_{2}$,etc.) and the theorem hierarchy ( thm-P, thm-NP, thm-$\Sigma^p_{2}$,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$_1$, C$_2$ 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 $F_1$ and $F_2$ be two PKR formalisms. If $F_1$ is in model-C and $F_2$ is model-C-hard, then there exists a poly-size reduction $f:F_1 \mapsto F_2$ satisfying model preservation.

Proof. Recall that since $F_1$ is in model-C, model checking in $F_1$ is in $\parallel\!\leadsto$ C, and since $F_2$ is model-C-hard, model checking in $F_1$ is non-uniformly comp-reducible to model checking in $F_2$. That is, (adapting Def. 6) there exist two poly-size binary functions $f_1$ and $f_2$, and a polynomial-time binary function $g$ such that for every pair ${\langle KB, M \rangle }$ it holds that

$$M \models_{F_1} KB \mbox{ if and only if } g(f_2(KB,\vert M\vert),M) \models_{F_2} f_1(KB,\vert M\vert)$$

(note that $g$ is the poly-time function appearing in Def. 6, different from $g_{KB}$ which is the poly-size circuit appearing in Def. 8).

Now observe that $\vert M\vert$ can be computed from $KB$ by simply counting the letters appearing in $KB$; let $f_3$ be such a counting function, i.e., $\vert M\vert = f_3 (KB)$. Clearly, $f_3$ is poly-size. Define the reduction $f$ as $f(KB)=f_1(KB,f_3 (KB))$. Since poly-size functions are closed under composition, $f$ is poly-size. Now we show that $f$ is a model-preserving reduction. By Definition 8, we need to prove that there exists a polynomial $p$ such that for each knowledge base $KB$ in $F_1$, there exists a poly-size circuit $g_{KB}$ such that for every interpretation $M$ of the variables of $KB$ it holds that $M \models_{F_1} KB$ iff $g_{KB}(M) \models_{F_2} f(KB)$.

We proceed as follows: Given a $KB$ in $F_1$, we compute $z=f_2(KB,\vert M\vert)= f_2(KB,f_3(KB))$. Since $f_2$ and $f_3$ are poly-size, $z$ has size polynomial with respect to $\vert KB\vert$. Define the circuit $g_{KB}(M)$ as the one computing $g(z,M) = g(f_2(KB,f_3(KB)),M)$. Since $g$ is a poly-time function over both inputs, and $z$ is poly-size in $KB$, there exists a representation of $g(z,M)$ as a circuit $g_{KB}$ whose size is polynomial wrt $KB$. From this construction, $M \models_{F_1} KB$ iff $g_{KB}(M) \models_{F_2} f(KB)$. 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 $F_1$ and $F_2$ be two PKR formalisms. If the polynomial hierarchy does not collapse, $F_1$ is model-C$_1$-hard, $F_2$ is in model-C$_2$, and C$_2 \subset$ C$_1$, then there is no poly-size reduction $f:F_1 \mapsto F_2$ satisfying model preservation.

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

$$\epsilon A = \{{\langle x, y \rangle } ~\vert~ x=\epsilon \mbox{~(the empty string) and~} y \in A \}$$

We already proved [6, Thm. 6] that $\epsilon A$ is $\parallel\!\leadsto$ C$_1$-complete. Since model checking in $F_1$ is model-C$_1$-hard, $\epsilon A$ is non-uniformly comp-reducible to model checking in $F_1$. That is, (adapting Def. 6) there exist two poly-size binary functions $f_1$ and $f_2$, and a polynomial-time binary function $g$ such that for every pair ${\langle \epsilon, y \rangle }$, it holds ${\langle \epsilon, y \rangle }\in \epsilon A$ if and only if $g(f_2(\epsilon,\vert y\vert),y) \models_{F_1} f_1(\epsilon,\vert y\vert)$. Let $\vert y\vert=n$. Clearly, the knowledge base $f_1(\epsilon,\vert y\vert)$ depends only on $n$, i.e., there is exactly one knowledge base for each integer. Call it $KB_n$. Moreover, $f_2(\epsilon,\vert y\vert)=f_2(\epsilon,n)$ also depends on $n$ only: call it $O_n$ (for Oracle). Observe that both $KB_{n}$ and $O_n$ have polynomial size with respect to $n$.

If there exists a poly-size reduction $f:F_1 \mapsto F_2$ satisfying model preservation, then given the knowledge base $KB_n$ there exists a poly-size circuit $h_n$ such that $g(O_n,y) \models_{F_1} KB_n$ if and only if $h_{n}(g(O_n,y)) \models_{F_2} f(KB_n)$.

Therefore, the $\parallel\!\leadsto$ C$_1$-complete problem $\epsilon A$ can be non-uniformly reduced to a problem in $\parallel\!\leadsto$ C$_2$ as follows: Given $y$, from its size $\vert y\vert=n$ one obtains (with a preprocessing) $f(KB_n)$ and $O_n$. Then one checks whether the interpretation $h_{n}(g(O_n,y))$ (computable in polynomial time given $n$, $y$ and $O_n$) is a model in $F_2$ for $f(KB_n)$. From the fact that model checking in $F_2$ is in $\parallel\!\leadsto$ C$_2$, we have that $\parallel\!\leadsto$ C$_1 \subseteq$ $\parallel\!\leadsto$ C$_2$. We proved in a previous paper that such result implies that C$_1$/poly $\subseteq$ C$_2$/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 ($F_1$) higher up in the hierarchy into one ($F_2$) in a lower class (Theorem 5). In the latter case we say that $F_1$ is more space-efficient than $F_2$.

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 $F_1$ and $F_2$ be two PKR formalisms. If $F_1$ is in thm-C and $F_2$ is thm-C-hard, then there exists a poly-size reduction $f:F_1 \mapsto F_2$ satisfying theorem preservation.

Proof. Recall that since $F_1$ is in thm-C, inference in $F_1$ is in $\parallel\!\leadsto$ C, and since $F_2$ is thm-C-hard, inference in $F_1$ is non-uniformly comp-reducible to inference in $F_2$. That is, (adapting Def. 6) there exist two poly-size binary functions $f_1$ and $f_2$, and a polynomial-time binary function $g_{1}$ such that for every pair ${\langle KB, \varphi \rangle }$ it holds that

$$KB \vdash_{F_1} \varphi \mbox{ if and only if } f_1(KB,\vert\varphi\vert) \vdash_{F_2} g(f_2(KB,\vert\varphi\vert),\varphi)$$

(here we distinguish the poly-time function $g$ appearing in Def. 6 and the poly-size circuit $g_{KB}$ appearing in Def. 9).

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

$$KB \vdash_{F_1} \varphi \mbox{ if and only if } f_1(KB,\vert KB\vert) \vdash_{F_2} g(f_2(KB,\vert KB\vert),\varphi)$$

Define the reduction $f$ as $f(KB)=f_1(KB,f_3 (KB))$, where $f_3$ is the poly-size function that computes the size of its input. Since poly-size functions are closed under composition, $f$ is poly-size.

Now, we show that $f$ is a theorem-preserving reduction, i.e.,$f$ satisfies Def. 9. This amounts to proving that for each knowledge base $KB$ in $F_1$ there exists a circuit $g_{KB}$, whose size is poynomial wrt $KB$, such that for every formula $\varphi$ on the variables of $KB$ it holds that $KB \vdash_{F_1} \varphi$ iff $f(KB) \vdash_{F_2} g_{KB}(\varphi)$.

We proceed as in the proof of Theorem 4: Given a $KB$ in $F_1$, let $z=f_2(KB,f_3(KB))$. Since $f_2$ and $f_3$ are poly-size, $z$ has polynomial size with respect to $\vert KB\vert$. Define $g_{KB}(\varphi) = g(z,\varphi) = g(f_2(KB,f_3(KB)),\varphi)$. Clearly, $g_{KB}$ can be represented by a circuit of polynomial size wrt $KB$. From this construction, $KB \vdash_{F_1} \varphi$ iff $f(KB) \vdash_{F_2} g_{KB}(\varphi)$. Hence, the claim follows. 

Theorem 7  

Let $F_1$ and $F_2$ be two PKR formalisms. If the polynomial hierarchy does not collapse, $F_1$ is thm-C$_1$-hard, $F_2$ is in thm-C$_2$, and C$_2 \subset$ C$_1$, then there is no poly-size reduction $f:F_1 \mapsto F_2$ satisfying theorem preservation.

Proof. We show that if such a reduction exists, then C$_1$/poly $\subseteq$ C$_2$/poly and the polynomial hierarchy collapses at some level [52]. Let $A$ be a complete problem for class C$_1$. Define the problem $\epsilon A$ as in the proof of Theorem 5: this problem is $\parallel\!\leadsto$ C$_1$-complete [6, Thm. 6]. Since inference in $F_1$ is thm-C$_1$-hard, $\epsilon A$ is non-uniformly comp-reducible to inference in $F_1$. That is, (adapting Def. 6) there exist two poly-size binary functions $f_1$ and $f_2$, and a polynomial-time binary function $g$ such that for every pair ${\langle \epsilon, y \rangle }$, ${\langle \epsilon, y \rangle }\in \epsilon A$ if and only if $f_1(\epsilon,\vert y\vert) \vdash_{F_1} g(f_2(\epsilon,\vert y\vert),y)$. Let $\vert y\vert=n$. Clearly, the knowledge base $f_1(\epsilon,\vert y\vert)$ depends just on $n$, i.e., there is one knowledge base for each integer. Call it $KB_n$. Moreover, also $f_2(\epsilon,\vert y\vert)=f_2(\epsilon,n)$ depends just on $n$: call it $O_n$ (for Oracle). Observe that both $KB_{n}$ and $O_n$ have polynomial size with respect to $n$.

If there exists a poly-size reduction $f:F_1 \mapsto F_2$ satisfying theorem preservation, then given the knowledge base $KB_n$ there exists a poly-time function $h_n$ such that $KB_n \vdash_{F_1} g(O_n,y)$ if and only if $f(KB_n) \vdash_{F_2} h_n(g(O_n,y))$.

Therefore, the $\parallel\!\leadsto$ C$_1$-complete problem $\epsilon A$ can be non-uniformly reduced to a problem in $\parallel\!\leadsto$ C$_2$ as follows: Given $y$, from its size $\vert y\vert=n$ one obtains (with an arbitrary preprocessing) $f(KB_n)$ and $O_n$. Then one checks whether the formula $h_n(g(O_n,y))$ (computable in poly-time given $y$ and $O_n$) is a theorem in $F_2$ of $f(KB_n)$. From the fact that inference in $F_2$ is in $\parallel\!\leadsto$ C$_2$, we have that $\parallel\!\leadsto$ C$_1 \subseteq$ $\parallel\!\leadsto$ C$_2$. It follows that C$_1$/poly $\subseteq$ C$_2$/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.