define the operation, decomposition, where the sharing of variables comes into consideration.

Consider a prenex formula, $f$, which has $n$ variables, out of which, there are $k$ quantified variables and $n-k$ quantifier-free variables. We say that the decomposition of $f$, $F$ is the set consisting of all the clauses which occur in the CNF of $f$.

This definition of decomposition defines separability as a property of the formula. In the remainder of this section, we assume that all prenex formulae are in variables, $x_1,. . .,x_n$. It is natural to classify prenex formulae into classes based on the number of clauses it can be separated into. Thus, we have the following definition.

A prenex formula is defined to be k-separable if its CNF has at least $k$ clauses. The set of all k-separable formulae shall be denoted by $S_k$.

According to this definition, we can observe that $S_k \subset S_{k-1}$. The set of 1-separable formulae is the set of all prenex formulae, which shall be denoted by $P$. We assume that we have only a constant number of processors, and we denote this by $K$. This leads to a definition of the class of separable problems.

Consider a set $S 