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?

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.