We assume a countable number of propositional variables and
the standard connectives
. A *literal* is
either a variable (*positive* literal) or its negation
(*negative* literal). A propositional formula is a well-formed formula
built on a finite number of variables and on the connectives;
denotes the set of variables that occur in the propositional formula .
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,
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 is a set of literals that
contains exactly one literal per variable in , and a *model* of
a propositional formula is an assignment to that
satisfies in the usual way, where assigns to iff
; we also write as a tuple, e.g., for
. We write for the value assigned
to by , and
for the set of all the
models of a propositional formula ; is said to be
*satisfiable* if
. A formula
is said to *imply* a propositional formula (written
) if
.
More generally, we identify sets of models with Boolean functions, and
use the notations
(negation),
(disjunction) and so on.

The notion of *projection* is very important for the rest of the
paper. For an assignment to a set of variables and ,
write for the set of literals in that are formed upon
, e.g.,
. Projecting a set of
assignments onto a subset of its variables intuitively consists in
replacing each assignment with ; for sake of simplicity
however, we define the projection of a set of models to be
built upon the same set of variables as . This yields the
following definition.

since .

Remark that the projection of the set of models of a formula onto a set of variables is the set of models of the most general consequence of that is independent of all the variables not in . Note also that the projection of onto is the set of models of the formula obtained from by forgetting its variables not occurring in . 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 denote two sets of assignments to the set of variables , and let . First, projection is distributive over disjunction, i.e., . Now it is distributive over conjunction when does not depend on the variables depends on, i.e., when there exist , with ( does not depend on ) and , holds; note that this is not true in the general case. Note finally that in general is not the same as .