Exactly-one constraint (source code)

= Exactly-one constraint
{title2=$\sum_{i=1}^{q}p_i=1$}

A restriction requiring exactly one member of a <set> of <Boolean variables> to be true. A direct <conjunctive normal form> encoding combines one at-least-one <Boolean clause>, $p_1\lor\cdots\lor p_q$, with $\binom q2$ at-most-one <Boolean clauses>, $\neg p_i\lor\neg p_j$ for $i<j$. The first supplies existence and the second supplies uniqueness. For $q=0$, the empty at-least-one <Boolean clause> correctly makes the condition unsatisfiable.