Questionnaire-2024/sat_solvers_dpll/3023_sol.tex

\item \ifassignmentsheet \points{2} \else \prac \fi Consider the propositional formula $\phi = (p \lor \lnot q) \imp (\lnot p \land \lnot r)$. Fill out the truth table for $\phi$
and its subformulas. Compute a CNF as well as a DNF for $\phi$ from
the truth table.

\begin{tabular}{|c|c|c||c|c|c|c|c||c|}
\hline
$p$ & $q$ & $r$ & $\lnot q$ & $p \lor \lnot q$ & $\lnot p$ & $\lnot r$ & $\lnot p \land \lnot r$ & $\phi = (p \lor \lnot q) \imp (\lnot p \land \lnot r)$\\
\hline
\hline%p   q   r     %!q     !p  !r      phi
      \F &\F &\F &    \T&\T &\T &\T &\T &\T\\ \hline
      \F &\F &\T &    \T&\T &\T &\F &\F &\F\\ \hline
      \F &\T &\F &    \F&\F &\T &\T &\T &\T\\ \hline
      \F &\T &\T &    \F&\F &\T &\F &\F &\T\\ \hline
      \T &\F &\F &    \T&\T &\F &\T &\F &\F\\ \hline
      \T &\F &\T &    \T&\T &\F &\F &\F &\F\\ \hline
      \T &\T &\F &    \F&\T &\F &\T &\F &\F\\ \hline
      \T &\T &\T &    \F&\T &\F &\F &\F &\F\\ \hline
\end{tabular}


The resulting CNF:
\begin{align*}
  (\clause{p;q;\lnot r})&~\land \\
  (\clause{\lnot p;q;r})&~\land \\
  (\clause{\lnot p;q;\lnot r})&~\land \\
  (\clause{\lnot p;\lnot q;r})&~\land \\
  (\clause{\lnot p;\lnot q;\lnot r})&
\end{align*}

The resulting DNF:

\begin{align*}
  (\cube{\lnot p;\lnot q;\lnot r})&~\lor \\
  (\cube{\lnot p;      q;\lnot r})&~\lor \\
  (\cube{\lnot p;      q;      r})&
\end{align*}