Logic - Proving or disproving a formula is satisfiable

Question

I want to find out if the formula $\{p\implies(q\land r),(p\lor r)\implies q,\neg r\}$ is satisfiable. (meanings each clause is satisfiable. there is an $\land$ between the clauses.

The problem is that the first (leftmost) clause is not a Horn clauses, so we can't use Horn's algorithm if I am not mistaken.

Is there another way to approach this?

Answer 1

We can rewrite $p \to (q \land r)$ as $\lnot p \lor (q \land r)$ [see Material Implication] and then apply Distributivity to get :

$[\lnot p \lor (q \land r)] \equiv [(\lnot p \lor q) \land (\lnot p \lor r)]$.

Thus, we can replace the formula with the couple of Horn clauses :

$\lnot p \lor q, \lnot p \lor r$.

---

The same approach can be aused with $(p ∨ r) \to q$, and the final result will be :

$\{ ¬p∨q, ¬p∨r, ¬r∨q, ¬r \}$

that is satisfiable: it is enough to set $p=r=FALSE$.