 Exactly-one constraint

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\vee \cdots \vee p_q$, with $\left(\genfrac{}{}{0ex}{}{q}{2}\right)$ at-most-one Boolean clauses, $\neg p_i\vee \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.