Conjunctive normal form (source code)

= Conjunctive normal form
{title2=$\bigwedge_i\bigvee_j\ell_{ij}$}

= CNF
{c}
{synonym}

A <Boolean formula> is in <conjunctive normal form> when it is a <logical conjunction> of <Boolean clauses>. It is true precisely when every <Boolean clause> is true under the same <Boolean valuation>; an empty <logical conjunction> is true. For example, $(x\lor\neg y)\land(z)$ has two <Boolean clauses> with widths two and one. Width counts <Boolean literal> occurrences within a <Boolean clause>, whereas the <Boolean clause> count counts the conjuncts. <2-SAT> bounds width by two, and <3-SAT> bounds width by three. A <Boolean formula> with an empty <Boolean clause> is an <unsatisfiable Boolean formula>.