The strength of the dominance rule

Leszek Aleksander Kołodziejczyk, Neil Thapen

It has become standard that, when a SAT solver decides that a CNF $\Gamma$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $\Gamma$ in some pro…