Proving using a SAT solver that KB entails D
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.