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.
How to Modify SAT Solvers to Produce Resolution Refutations for Unsatisfiable Instances?
algorithms;sat solvers
If you know something about CDCL conflict clause generation, you will know that they are produced by resolution per se. For example, on page 137 of Handbook of Satisfiability, clause learning is done by the following procedure:$$\omega_L^{d,i}=\begin{cases}\alpha(\kappa)&{\rm if\ }i=0\\\omega_L^{d,i-1}\odot\alpha(l)&{\rm if\ }i\ne0\land\xi(\omega_L^{d,i-1},l,d)=1\\\omega_L^{d,i-1}&{\rm if\ }i\ne0\land\forall_l\xi(\omega_L^{d,i-1},l,d)=0\end{cases}$$Here, $\alpha(v)$ is the antecedent of $v$. The first line specifies the base case. The recursion will ensue following the second line. The third line signals a fixed point and the process halts. Note in the second line, $\odot$ signifies resolution.So just print the generation process and you will get a resolution refutation of the unsatisfiable formula.