= Partial Boolean assignment
{title2=$v:S\to\{0,1\},\quad S\subseteq\operatorname{Var}(F)$}
A <partial Boolean assignment> gives <truth values> to some of a <Boolean formula>'s <Boolean variables>. An extension is a complete <Boolean valuation> agreeing on the assigned <Boolean variables>. In <CNF>, a <Boolean clause> containing a true assigned <Boolean literal> is already satisfied; a <Boolean clause> whose every <Boolean literal> is assigned false rules out all extensions. A <Boolean clause> with no true assigned <Boolean literal> and at least one unassigned <Boolean variable> is unresolved. An unresolved <Boolean clause> need not have a compatible extension with the other <Boolean clauses>.
For $F$ in <Boolean satisfiability problem>, setting $x=y=0$ already falsifies $C_1$, so both choices of $z$ can be discarded. Setting only $x=0$ leaves $C_1$ unresolved and forces $y=1$ if a <satisfying assignment> is to survive; then $C_3$ forces $z=0$. Branching on an unassigned <Boolean variable> into its two <truth values> and discarding branches with a false <Boolean clause> is sound: every <satisfying assignment> follows one branch and cannot extend a false <Boolean clause>. If all branches are eliminated, the original <Boolean formula> is an <unsatisfiable Boolean formula>.
Back to article page
