Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas

Question

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:

• Ben-Sasson, Eli, and Avi Wigderson. "Short proofs are narrow—resolution made simple." Proceedings of the thirty-first annual ACM symposium on Theory of computing. 1999.

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

• Albert Atserias, Víctor Dalmau, A combinatorial characterization of resolution width, Journal of Computer and System Sciences, Volume 74, Issue 3, 2008

• A. Atserias, "Unsatisfiable random formulas are hard to certify," Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, 2002, pp. 325-334, doi: 10.1109/LICS.2002.1029840

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.

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.