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 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.