LGT Sheet

Question 1

Apply DPLL algorithm to clauses:

$$\begin{array}{c}(Q\vee \neg R\vee \neg S\vee X),(\neg Q\vee \neg R),(R\vee \neg S),(P\vee \neg R\vee T\vee X)\\ (\neg P\vee \neg Q\vee \neg X),(S\vee X),(Q\vee \neg X),(\neg Q\vee \neg X)\end{array}$$

Branch on $\neg X$:

$$\begin{array}{c}(Q\vee \neg R\vee \neg S),(\neg Q\vee \neg R),(R\vee \neg S),(P\vee \neg R\vee T\vee X),S\end{array}$$

Eliminate $S$:

$$\begin{array}{c}(Q\vee \neg R),(\neg Q\vee \neg R),R,(P\vee \neg R\vee T\vee X)\end{array}$$

Eliminate $R$:

$$\begin{array}{c}Q,\neg Q,(P\vee \neg R\vee T\vee X)\end{array}$$

Not satisfiable as the other branch would also lead to a contradiction.