Given a formula $\varphi$ in propositional logic, we say that  $\varphi$ is
\emph{satisfiable} if it has a model in which is evaluates to \emph{true}.
We say that $\varphi$ is
\emph{unsatisfiable} if there is no model under which $\varphi$ evaluates to \emph{true}.