How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?

In recent SAT competitions, there is a Certified UNSAT track. The problem instances are all unsatisfiable and the solvers are asked to produce certificates for unsatisfiability. One way is to produce a resolution refutation for the set of clauses in a problem instance. How can a SAT solver, say MiniSAT, be modified to do this? Can this be done for every solver? I searched the Internet and found little information. A reference is good for me.

A clause-learning SAT solver can be described approximately as follows. There is a stash of learned clauses, which starts empty. We run a recursive procedure, which at each point in time, first checks whether the current assignment (initially empty) contradicts an axiom or something in the stash. If so, there is no need to explore this branch. Otherwise, it picks a variable, and tries both assignment recursively. When a recursive call corresponding to a partial assignment $\alpha$ returns, we learn the clause $\lnot \alpha$. At any given point in time we are allowed to forget clauses. (It's important for the proof that each clause is learned, even if we forget it later on).

We now take the transcript of the algorithm and consider the clauses in the order in which they are learned. We prove that whenever a clause $c$ is learned, it can be derived using the rules of resolution from existing clauses or from axioms; in particular, at the very end we derive contradiction.

We allow the weakening rule in the refutation we construct; we can always get rid of weakening later on without increasing the refutation length (exercise).

There are three cases to consider. If the clause $c$ was learned because the corresponding assignment contradicted an axiom $c'$ or a clause in the stash $c'$, then $c$ is a weakening of $c'$. The interesting case is when $c = \lnot \alpha$ was learned since both assignment to some variable $x$ failed to produce a satisfying assignment. These assignments correspond to the learned clauses $c \lor x$ and $c \lor \lnot x$, from which $c$ follows by resolution.

Note that if we never use clauses in the stash then the resulting refutation is tree-like (every clause is used once), assuming we state each axiom whenever it's needed (rather than once and for all). Also, in any case the size (number of lines) of the refutation is the same as the number of recursive calls.

StackExchange Computer Science Q#56653, answer score: 5