Let $\varphi$ be a propositional formula defined over Boolean variables $x_1, . . . ,x_n$. \begin{itemize} \item A \emph{literal} is one of the variables $x_i$ or the negation of a variable, e.g., $x_1$. \item A \emph{clause} is a disjunction of literals, e.g., $x_1 \vee x_2$. \item A \emph{cube} is a conjunction of literals, e.g., $x_1 \wedge x_2$. \end{itemize}