The classical approach to solving the satis?ability problem of propositional logic prunes unsatis?able branches from the search space. We prune more agressively by also removing certain branches for which there exist other branches that are more satis?able. This is achieved by extending the popular con?ict-driven clause learning (CDCL) paradigm with so-called PR-clause learning. We implemented our new paradigm, named satisfaction-driven clause learning (SDCL), in the SAT solver Lingeling. Experiments on the well-known pigeon hole formulas show that our method can automatically produce proofs of unsatis?ability whose size is cubic in the number of pigeons while plain CDCL solvers can only produce proofs of exponential size.