"State of the art" algorithms deciding entailment of propositional formulas?

Question

I fail to find much about how to efficiently calculate whether a propositional formula entails another.

Considering the following two points...

1. We can check, for each truth assignment which makes the first formula true, whether it also makes the second true. If all of them do, the first entails the second. It works for disjunctive normal forms, conjunctive normal forms, ... anything really. But this can be prohibitively expensive for large numbers of propositions.
2. If we translate both formulas to disjunctive normal form we can more efficiently check for entailment, but we need to do the transformation to DNF first.

... what are the best algorithms to check entailment?

I was under the impression that this must be a problem that's long been solved, but where are the papers that deal with entailment of arbitrary propositional formulas? How do I calculate a yes/no answer without using DNFs?

Answer 1

Checking whether $P \Rightarrow Q$ is the same as checking that $P \land \lnot Q$ is unsatisfiable. Using the 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.