# Efficient transformation of clausal proof into resolution proof

Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the pigeon hole problem).

How can a clausal proof efficiently (i.e. in polynomial time) be converted to a resolution proof?

Is there any relationship between the size of the clausal proof and the corresponding size of the transformed resolution proof?

• Could you add some definitions? CDCL SAT solvers produce resolution proofs, which consists in clauses. – Mikolas Aug 23 '18 at 12:59