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