22/110
\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}