Counting Satisfying Assignments of a Propositional Formula

A propositional formula over $n$ atomic variables $x_1,\ldots,x_n$ has $2^{n}$ possible truth assignments. Counting how many make the formula true is the heart of many konkur logic problems. You rarely need the full truth table — exploit structure.

Three counting strategies

1. Independence / product rule. If the truth value of one sub‑formula is independent of a set of $k$ variables, those $k$ variables are free: each fixed satisfying pattern of the rest spreads over $2^{k}$ assignments. Multiply.
2. Case split on a shared sub‑formula. When a formula is $\bigwedge_i (\,H \vee L_i\,)$ — every clause shares a head $H$ — split on $H$:
   • $H$ true $\Rightarrow$ every clause is automatically true (the other literals are free).
   • $H$ false $\Rightarrow$ each clause collapses to its remaining part $L_i$, which must all hold. Add the two disjoint counts.
3. Complement (count the falsifying ones). For a single clause (a big OR) it is easier to count the one assignment of its literals that makes it false, then subtract.

Key formulas

For a disjunction (clause) of $r$ distinct literals over its own $r$ variables, exactly one of the $2^{r}$ literal‑patterns is false (every literal false), so

$\#\{\text{satisfying}\} = 2^{r}-1 \quad(\text{over those } r \text{ variables}).$

If $j$ of the $n$ variables don't appear in the (sub)formula, multiply any count by $2^{j}$ for the free variables.

Worked mini‑example

Count the satisfying assignments of $(x_1 \vee x_2)\wedge(\sim x_1 \vee x_3)$ over $x_1,x_2,x_3$ (so $2^3=8$ total). Split on $x_1$:

The cases are disjoint, so $2+2=4$ assignments are satisfying (and indeed $4$ of $8$ — this formula is "$x_1\Rightarrow x_3$ and $\neg x_1 \Rightarrow x_2$").

Exam trick: when every clause of a CNF shares a common head $H$, never expand the whole truth table — split once on $H$. The $H=\text{true}$ branch frees all the other variables ($\times 2^{k}$), and only the small $H=\text{false}$ branch needs real work. Adding two disjoint cases beats checking $2^{n}$ rows.