TAOCP 7.1.1 Exercise 38
Let the given function in disjunctive normal form be f = C_1 \vee C_2 \vee \cdots \vee C_m, where each clause $C_i$ is a conjunction of literals of the form $x_j$ or $\bar{x}_j$.
Exercise 38. [25] Is it hard to test the satisfiability of functions in disjunctive normal form?
Verified: yes
Solve time: 59s
Solution
Let the given function in disjunctive normal form be
$$ f = C_1 \vee C_2 \vee \cdots \vee C_m, $$
where each clause $C_i$ is a conjunction of literals of the form $x_j$ or $\bar{x}_j$.
The function $f$ is satisfiable if and only if there exists an assignment of the variables such that at least one clause $C_i$ evaluates to $1$. Since $\vee$ corresponds to Boolean disjunction, the value of $f$ under any assignment is $1$ if and only if at least one $C_i$ evaluates to $1$ under that assignment.
Fix a clause $C_i$. Write it as a conjunction
$$ C_i = \ell_{i1} \wedge \ell_{i2} \wedge \cdots \wedge \ell_{ik_i}, $$
where each $\ell_{ij}$ is a literal. The clause $C_i$ is satisfiable if and only if no variable $x$ appears both as $x$ and as $\bar{x}$ among the literals $\ell_{i1}, \ldots, \ell_{ik_i}$. If such a contradiction occurs, then $C_i$ contains a factor $x \wedge \bar{x}$, which is $0$ for every assignment, hence $C_i$ is unsatisfiable. Conversely, if no such contradictory pair occurs, an assignment can be defined by setting every variable appearing unnegated in $C_i$ to $1$, every variable appearing negated to $0$, and the remaining variables arbitrarily; under this assignment each literal in $C_i$ is $1$, hence $C_i = 1$.
Therefore $f$ is satisfiable if and only if at least one clause $C_i$ contains no variable appearing in both polarities.
Testing this condition requires scanning each clause and checking whether any variable occurs twice with opposite signs. Each occurrence of a variable contributes to at most one check against its complement within the same clause. Hence the test reduces to verifying, for each $C_i$, whether the sets of positive and negative literals are disjoint.
Since $f$ is satisfiable if and only if some clause passes this test, the satisfiability problem for DNF reduces to checking all clauses and accepting if a consistent clause exists.
This completes the proof. ∎