Question 1 Old

$F=(P\vee Q)\wedge (\neg P\vee \neg Q)\wedge (\neg P\vee Q)\wedge (R\vee S)\wedge (R\vee T\vee U)$

$(P\vee Q),(\neg P\vee \neg Q),(\neg P\vee Q),(R\vee S),(R\vee T\vee U)$

• Start with unit clause elimination, nothing can be eliminated.
• Next check for pure literals, there are several: $R,S,T,U$. Lets pick $R$ and set it to $\top$. $(\neg P\vee Q),(P\vee \neg Q),(P\vee Q),\cancel{(R\vee S)},\cancel{(R\vee T\vee U)}$ This eliminates two clauses and four variables.
• There are no other pure literals or unit clauses. Hence, we should branch on some variable, say $P$.
  • Let $P$ be $\perp$. Hence eliminate clauses with $\neg P$ and remove $P$ from clauses. $\cancel{(\neg P\vee Q)},(\cancel{P\vee }\neg Q),(\cancel{P\vee }Q)$ This leaves us with: $\neg Q,Q$ This is a contradiction hence we backtrack.
  • Let $P$ be $\top$. Hence eliminate clauses with $P$ and remove $\neg P$ from clauses. $(\cancel{\neg P\vee }Q),\cancel{(P\vee \neg Q)},\cancel{(P\vee Q)}$ This leaves us with just $Q$. Now we recursively call the DPLL algorithm:
    • Start with unit clause elimination, there is one $Q$. We let $Q$ be $\top$. $\cancel{Q}$ Hence we are left with: $\varnothing$ Therefore the algorithm terminates successfully and $F$ is satisfiable.