<p>Partially answering question (2), the Prover-Delayer game of Atserias and Dalmau can be interpreted as a more general &quot;dag-like query complexity&quot; specialized to CNFs. See e.g. <a href="https://dblp.org/rec/journals/toc/GargGK020" rel="nofollow noreferrer">GGKS'18</a>. And the matching game in the paper of Atserias has connections to questions in network switching. See <a href="https://dblp.org/rec/journals/siamdm/FeldmanFP88" rel="nofollow noreferrer">FFP'88</a>.</p>

CC BY-SA 4.0
2023-09-07T04:06:12.347Z
2023-09-07T04:06:12.347Z
notautogenerated
<p>Recall that the <strong>width</strong> of a resolution refutation <span class="math-container">$R$</span> of a CNF formula <span class="math-container">$F$</span> is the maximal number of literals in any clause occurring in <span class="math-container">$R$</span>. I am intersting in finding the minimal <strong>width</strong> of some certain unsatisfiable SAT formulas</p>
<p>I'm aware of two methods to find minimal <strong>width</strong> mentioned in academic papers:</p>
<ul>
<li>Ben-Sasson, Eli, and Avi Wigderson. &quot;<a href="https://www.researchgate.net/publication/2370656_Short_Proofs_are_Narrow_-_Resolution_made_Simple" rel="nofollow noreferrer">Short proofs are narrow—resolution made simple.</a>&quot; Proceedings of the thirty-first annual ACM symposium on Theory of computing. 1999.</li>
</ul>
<p>which provides a method to determine resolution refutation width, primarily applicable to clauses and XOR SAT.</p>
<ul>
<li><p>Albert Atserias, Víctor Dalmau,
<a href="https://www.sciencedirect.com/science/article/pii/S0022000007000876" rel="nofollow noreferrer">A combinatorial characterization of resolution width</a>,
Journal of Computer and System Sciences,
Volume 74, Issue 3,
2008</p>
</li>
<li><p>A. Atserias, &quot;<a href="https://ieeexplore.ieee.org/document/1029840" rel="nofollow noreferrer">Unsatisfiable random formulas are hard to certify</a>,&quot; Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, 2002, pp. 325-334, doi: 10.1109/LICS.2002.1029840</p>
</li>
</ul>
<p>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.</p>
<p><strong>My question:</strong></p>
<ol>
<li>Is there any other methods to find minimal width?</li>
<li>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.</li>
</ol>

<reference-request><sat><proof-complexity><csp><resolution>
Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas
Jxb
# Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas

(Asked by: username_0 on 2023-09-04)

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.](https://www.researchgate.net/publication/2370656_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](https://www.sciencedirect.com/science/article/pii/S0022000007000876),
  Journal of Computer and System Sciences,
  Volume 74, Issue 3,
  2008
* A. Atserias, "[Unsatisfiable random formulas are hard to certify](https://ieeexplore.ieee.org/document/1029840)," 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.

**Tags:** reference-request, sat, proof-complexity, csp, resolution


---

## 1 answers

### Answer by username_1 on 2023-09-07. Score: 2

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](https://dblp.org/rec/journals/toc/GargGK020). And the matching game in the paper of Atserias has connections to questions in network switching. See [FFP'88](https://dblp.org/rec/journals/siamdm/FeldmanFP88).


---

