# Proving using a SAT solver that KB entails D

Suppose you're given this KB:

$$KB = (A, A ⇒ B, A ⇒ C, B ∧ C ⇒ D)$$

How would you show using a SAT solver that $$KB \vDash D$$?

## 1 Answer

TL;DR: Use the SAT solver to search for a counterexample.

To check that $$KB \models \varphi$$, you need to know whether there is any assignment that is consistent with $$KB$$ but that does not satisfy $$\varphi$$. In other words, you need to know whether $$KB \land \neg \varphi$$ is satisfiable or not. If $$KB \land \neg \varphi$$ is satisfiable, then you have found a counterexample that demonstrates that $$KB \not\models \varphi$$. If $$KB \land \neg \varphi$$ is not satisfiable, then you proven that $$KB \models \varphi$$ is true.

Now apply that to your specific example.