x|a|b & ~x|c|d → a|b|c|d
Solutions carry forward under resolution. Suppose resolution produces an empty clause, the join of x and ~x. If e had a solution, the same solution is valid after resolution, all the way to the expression that contains x and ~x. This is a contradiction, hence e cannot be satisfied. Resolving to an empty clause implies no solution.
Conversely, assume e is a boolean expression with the fewest number of variables, such that e has no solution, yet resolution does not produce an empty clause. If e contains only one variable, and it has no solution, then it looks like x & ~x, and resolution yields an empty clause. Thus there are at least two variables in e.
Choose any variable, such as x. Set x to true and delete the clauses containing x, and delete the atoms ~x. What remains cannot be satisfied, hence it yields an empty clause. Record the successive resolutions that lead to an empty clause. Now bring ~x back in. At some point one of the resolved clauses introduces the atom ~x, and it persists to the end, making the empty clause into the singleton clause ~x.
Set x to false and run the same procedure. This time resolution produces the singleton clause x. Together, x and ~x produce the empty clause. Therefore a conjunctive normal form boolean expression is unsatisfyable iff resolution yields an empty clause.
Alas, this doesn't lead to a polynomial time procedure. The path to an empty clause is uncertain, and if you apply resolution wherever you can, the number of clauses can grow exponentially. However, computer programs often employ directed resolution, using an assortment of heuristics, to search for an empty clause - and this approach is more successful than you might first think. If you are interested in automated reasoning, you need to look at otter.