Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then the length of the proof is polynomially bounded, since there are only $O(n^k)$ distinct $k$-clauses over $n$ variables. We say a resolution proof is narrow if its width is $3$. I've written a program to decide whether an input unsatisfiable 3-CNF has a narrow resolution proof. I generated millions of unsatisfiable 3-CNFs randomly with $n=4,5,6$ and found all of them have narrow resolution proofs. I also tried the 3-CNF version of the propositional pigeonhole principle, and found that when there are $4$ pigeons, the formula has an narrow proof; while for $5$ pigeons, there isn't a narrow proof. However, the $5$-pigeon pigeonhole principle formula has $25$ variables and $50$ clauses, and I guess it's not the shortest formula that can't be refuted by narrow resolution.
I have the following questions:
- Are there any researches conducted on this problem, i.e., the shortest formulas that can't be refuted by narrow resolution?
- Is there a better way to search for these formulas than random generation?
Update 07/02/2023:
I've constructed an unsatisfiable 3-CNF formula with $5$ variables which cannot be refuted by narrow resolution:
$$ (a\lor b\lor c)\land\\(a\lor b\lor d)\land\\(a\lor b\lor e)\land\\(a\lor c\lor d)\land\\(a\lor c\lor e)\land\\(a\lor d\lor e)\land\\(b\lor c\lor d)\land\\(b\lor c\lor e)\land\\(b\lor d\lor e)\land\\(c\lor d\lor e)\land\\(\neg a\lor\neg b\lor\neg c)\land\\(\neg a\lor\neg b\lor\neg d)\land\\(\neg a\lor\neg b\lor\neg e)\land\\(\neg a\lor\neg c\lor\neg d)\land\\(\neg a\lor\neg c\lor\neg e)\land\\(\neg a\lor\neg d\lor\neg e)\land\\(\neg b\lor\neg c\lor\neg d)\land\\(\neg b\lor\neg c\lor\neg e)\land\\(\neg b\lor\neg d\lor\neg e)\land\\(\neg c\lor\neg d\lor\neg e) $$
