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$. For every $w$, there are unsatisfiable formulas $F$ in 3-CNF s.t. every resolution refutation of $F$ requires width at least $w$.
I need a concrete example of an unsatisfiable formula in 3-CNF (as small and simple as possible) that has no resolution refutation of width 4.
The following example comes from the paper which gives a combinatorial characterization of resolution width by Atserias and Dalmau (Journal, ECCC, author's copy).
Theorem 2 of the paper states that, given a CNF formula $F$, resolution refutations of width at most $k$ for $F$ are equivalent to winning strategies for Spoiler in the existential $(k+1)$-pebble game. Recall that the existential pebble game is played between two competing players, called Spoiler and Duplicator, and the positions of the game are partial assignments of domain size at most $k+1$ to variables of $F$. In the $(k+1)$-pebble game, starting from the empty assignment, Spoiler wants to falsify a clause from $F$ while remembering at most $k+1$ boolean values at a time, and Duplicator wants to prevent Spoiler from doing so.
The example is based on (the negation of) the pigeonhole principle.
For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{1, \dotsc, n \}$, let $p_{i,j}$ be a propositional variable meaning that pigeon $i$ sits in hole $j$. For every $i \in \{1, \dotsc, n+1 \}$ and $j \in \{0, \dotsc, n \}$, let $y_{i,j}$ be a new propositional variable. The following $3$-CNF formula ${EP}_i$ expresses that pigeon $i$ sits in some hole: $$ {EP}_i \equiv \neg y_{i,0} \wedge \bigwedge_{j=1}^n (y_{i,j-1} \vee p_{i,j} \vee \neg y_{i,j} ) \wedge y_{i,n}. $$ Finally, the $3$-CNF formula ${EPHP}_n^{n+1}$ expressing the negation of the pigeonhole principle is the conjunction of all ${EP}_i$ and all clauses $H_k^{i,j} \equiv \neg p_{i,k} \vee \neg p_{j,k}$ for $i,j \in \{1, \dotsc, n+1 \}, i \ne j$ and $k \in \{1, \dotsc, n \}$.
Lemma 6 of the paper gives a fairly short and intuitive proof that Spoiler cannot win the $n$-pebble game on ${EPHP}_n^{n+1}$, hence ${EPHP}_n^{n+1}$ has no resolution refutation of width at most $n-1$.
The paper has another example in Lemma 9, based on the dense linear order principle.
Given that computing the minimum width for resolution refutations is EXPTIME-complete, and moreover it takes $\Omega(n^{(k-3)/12})$ time to certify that the minimum width is at least $k+1$ (see Berkholz's paper in FOCS or arXiv), perhaps it is hard to come up with examples which provably need wide resolution refutations?
