Comment modifier les solveurs SAT pour produire des réfutations de résolution pour des cas insatisfaisants?

Question

Dans les récentes compétitions SAT, il y a une piste certifiée UNSAT. Les cas de problème ne sont pas insatisfaisants et les résolveurs sont invités à produire des certificats pour insatisfaction. Une façon consiste à produire une réfutation de résolution pour l'ensemble des clauses dans un cas de problème. Comment un solveur SAT, dire Minisat, peut-il être modifié pour ce faire? Cela peut-il être fait pour chaque solveur? J'ai fouillé sur Internet et trouvé peu d'informations. Une référence est bonne pour moi.