\begin{frame}{Satisfiability in Propositional Logic} A formula of propositional logic consists of \begin{talign} \texttt{true} && \text{conjunction } \wedge && \text{variables} \\ \texttt{false} && \text{disjunction } \vee && \text{negation } \neg \end{talign}\vspace{-3ex} \begin{goal}{} A formula of propositional logic $\phi$ is \emph{satisfiable} if there exists an assignment of \texttt{true} and \texttt{false} to the variables such that $\phi$ evaluates to \texttt{true}. \end{goal} \pause\medskip \begin{block}{Theorem} Satisfiability of formulas of propositional logic is in NP. \end{block} \pause \begin{proof} We can construct a nondeterministic Turing machine that \begin{itemize} \item guesses an assignment of \texttt{true} and \texttt{false} to the variables, \item evaluates the formula (in polynomial time), and \end{itemize} accepts if the evaluation is \texttt{true}. \end{proof} \end{frame}