Recall that the width of a resolution refutation $R$ of a CNF formula $F$ is the maximal number of literals in any clause occurring in $R$. I am intersting in finding the minimal width of some certain unsatisfiable SAT formulas

I'm aware of two methods to find minimal width mentioned in academic papers:

which provides a method to determine resolution refutation width, primarily applicable to clauses and XOR SAT.

Atserias and Dalmau's method is comprehensive and encompasses a broader range of CNF formulas. They provide examples like pigeonhole and random SAT in their paper.

My question:

  1. Is there any other methods to find minimal width?
  2. For Albert Atserias' method, I am interested in exploring more practical examples or applications of this method. If you have any additional examples or references where this method has been successfully applied, please share them.

1 Answer 1


Partially answering question (2), the Prover-Delayer game of Atserias and Dalmau can be interpreted as a more general "dag-like query complexity" specialized to CNFs. See e.g. GGKS'18. And the matching game in the paper of Atserias has connections to questions in network switching. See FFP'88.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.