Preliminaries

We assume a countable number of propositional variables $x_1,x_2\dots$ and the standard connectives $\neg,\wedge,\vee,\oplus,\rightarrow,\leftrightarrow$. A literal is either a variable $x_i$ (positive literal) or its negation $\neg x_i$ (negative literal). A propositional formula is a well-formed formula built on a finite number of variables and on the connectives; $Var(\phi)$ denotes the set of variables that occur in the propositional formula $\phi$. A clause is a finite disjunction of literals, and a propositional formula is in Conjunctive Normal Form (CNF) if it is written as a finite conjunction of clauses. For instance, $\phi=(x_1\vee\neg x_2)\wedge(\neg x_1\vee x_2\vee\neg x_3)$ is in CNF. The dual notions of clause and CNF are the notions of term (finite conjunction of literals) and Disjunctive Normal Form (DNF) (finite disjunction of terms).

An assignment to a set of variables $V$ is a set of literals $m$ that contains exactly one literal per variable in $V$, and a model of a propositional formula $\phi$ is an assignment $m$ to $Var(\phi)$ that satisfies $\phi$ in the usual way, where $m$ assigns $1$ to $x_i$ iff $x_i\in m$; we also write $m$ as a tuple, e.g., $0010$ for $\{\neg x_1,\neg x_2,x_3,\neg x_4\}$. We write $m[i]$ for the value assigned to $x_i$ by $m$, and ${\mathcal M}(\phi)$ for the set of all the models of a propositional formula $\phi$; $\phi$ is said to be satisfiable if ${\mathcal M}(\phi)\neq\emptyset$. A formula $\phi$ is said to imply a propositional formula $\phi'$ (written $\phi\models\phi'$) if ${\mathcal M}(\phi)\subseteq{\mathcal M}(\phi')$. More generally, we identify sets of models with Boolean functions, and use the notations $\overline{{\mathcal M}}$ (negation), ${\mathcal M}\vee{\mathcal M'}$ (disjunction) and so on.

The notion of projection is very important for the rest of the paper. For $m$ an assignment to a set of variables $V$ and $A\subseteq V$, write $Select_A(m)$ for the set of literals in $m$ that are formed upon $A$, e.g., $Select_{\{x_1,x_2\}}(0110)=01$. Projecting a set of assignments onto a subset $A$ of its variables intuitively consists in replacing each assignment $m$ with $Select_A(m)$; for sake of simplicity however, we define the projection of a set of models ${\mathcal M}$ to be built upon the same set of variables as ${\mathcal M}$. This yields the following definition.

Definition 1 (projection)   Let $V=\{x_1,\dots,x_n\}$ be a set of variables, ${\mathcal M}$ a set of assignments to $V$ and $A\subseteq V$. The projection of ${\mathcal M}$ onto $A$ is the set of assignments to $V$ ${\mathcal M}_{\vert A}= \{m\ \vert\ \exists m'\in{\mathcal M},Select_A(m')=Select_A(m)\}$.

For instance, let ${\mathcal M}=\{0001,0010,0111,1100,1101\}$ be a set of assignments to $V=\{x_1,x_2,x_3,x_4\}$, and let $A=\{x_1,x_2\}$. Then it is easily seen that

$${\mathcal M}_{\vert A} = \{0000,0001,0010,0011\}\cup \{0100,0101,0110,0111\}\cup \{1100,1101,1110,1111\}$$

since $\{Select_A(m)\,\vert\,m\in{\mathcal M}\}=\{00,01,11\}$.

Remark that the projection of the set of models of a formula $\phi$ onto a set of variables $A$ is the set of models of the most general consequence of $\phi$ that is independent of all the variables not in $A$. Note also that the projection of ${\mathcal M}(\phi)$ onto $A$ is the set of models of the formula obtained from $\phi$ by forgetting its variables not occurring in $A$. For more details about variable forgetting and independence we refer the reader to the work by Lang et al. [LLM02].

It is useful to note some straightforward properties of projection. Let ${\mathcal M},{\mathcal M'}$ denote two sets of assignments to the set of variables $V$, and let $A\subseteq V$. First, projection is distributive over disjunction, i.e., $({\mathcal M}\vee{\mathcal M'})_{\vert A} = {\mathcal M}_{\vert A}\vee{\mathcal M'}_{\vert A}$. Now it is distributive over conjunction when ${\mathcal M}$ does not depend on the variables ${\mathcal M'}$ depends on, i.e., when there exist $A,A'\subseteq V$, $A\cap A'=\emptyset$ with ${\mathcal M}_{\vert A}={\mathcal M}$ (${\mathcal M}$ does not depend on $V\backslash A$) and ${\mathcal M'}_{\vert A'}={\mathcal M'}$, $({\mathcal M}\wedge{\mathcal M'})_{\vert A} = {\mathcal M}_{\vert A}\wedge{\mathcal M'}_{\vert A}$ holds; note that this is not true in the general case. Note finally that in general $(\overline{{\mathcal M}})_{\vert A}$ is not the same as $\overline{{\mathcal M}_{\vert A}}$.