# Tag Info

You haven't explained what $|\varphi|$ is, so let's guess that it is the number of clauses. So you are given a CNF $C_1 \land \cdots \land C_n$ in which each clause contains at least $\log_2 n$ distinct literals. Any clause which contains both a variable and its negation is always satisfied, so we can remove such clauses; call them spurious. Suppose that the ...
The claim is false. Let $\varphi = (x_1 \vee x_2) \wedge (\overline{x}_1 \vee x_2) \wedge (x_1 \vee \overline{x}_2) \wedge (\overline{x}_1 \vee \overline{x}_2)$. Here $|\varphi|=4$, each clause in $\varphi$ contains exactly $\log_2 |\varphi|=2$ distinct literals, yet $\varphi$ is not satisfiable. (This is also a counterexample if $|\varphi|$ denotes the ...