Checking whether $P \Rightarrow Q$ is the same as checking that $P \land \lnot Q$ is unsatisfiable. Using the [Tseytin transformation](https://en.wikipedia.org/wiki/Tseytin_transformation), you can convert $P \land \lnot Q$ into a form suitable for a SAT solver.

Conversely, satisfiability is a special case of your problem, since $P \Rightarrow \bot$ iff $P$ is unsatisfiable.