= Clause of a Boolean formula
{title2=$\ell_1\lor\cdots\lor\ell_k$}
= Clause
{synonym}
= Boolean clause
{c}
{synonym}
= Clauses of a Boolean formula
{synonym}
A <Boolean clause> is an expression $\ell_1\lor\cdots\lor\ell_k$ formed from <Boolean literals>, true when at least one <Boolean literal> is true. The empty <Boolean clause> is false. Repeating a <Boolean literal> does not change the <truth value>. A <CNF> <Boolean formula> is a <logical conjunction> of these <Boolean clauses>.
For $(\neg x\lor z)$, the only failing pair is $(x,z)=(1,0)$: its two <Boolean literals> then both have <truth value> zero. The one-<Boolean literal> <Boolean clause> $(x)$ requires $x=1$. A <Boolean clause> containing both $x$ and $\neg x$ is a <tautology>, since one of those <Boolean literals> is true under every <Boolean valuation>. These observations separate <Boolean clause> satisfaction from the simultaneous satisfaction required by <SAT>.
Back to article page
