Формула 3-CNF, которая требует ширины разрешения

Напомним , что ширина резолюции опровержение $R$ из формулы CNF $F$ представляет максимальное число литералов в любом пункте , происходящих в $R$ . Для каждого в 3-CNF $w$есть неудовлетворительные формулы $F$ каждое опровержение разрешения $F$ требует ширины не менее $w$ .

Мне нужен конкретный пример неудовлетворительной формулы в 3-CNF (настолько малой и простой, насколько это возможно), у которой нет опровержения разрешения ширины 4.

Следующий пример взят из статьи, в которой Асериас и Далмау дают комбинаторную характеристику ширины разрешения ( журнал , ECCC , авторская копия ).

Теорема 2 статьи гласит, что при заданной формуле CNF опровержения разрешения ширины не более k для F эквивалентны выигрышным стратегиям для Спойлера в игре с экзистенциальной ( k + 1 ) -пебблью. Напомним , что экзистенциальный галька игра играется между двумя конкурирующими игроками, называемых Спойлер и Дубликатор и позиции игры частичные задания размера домена в большинстве к + 1 к переменным F . В игре ( k + 1 ) -pebble, начиная с пустого задания, Спойлер хочет фальсифицировать предложение из $F$$k$$F$$(k+1)$$k+1$$F$$(k+1)$$F$запоминая не более логических значений за раз, и Duplicator хочет помешать Спойлеру сделать это.$k+1$

Пример основан на (отрицании) принципа голубиных отверстий.

Для каждого и j ∈ { 1 , … , n } пусть p i , j - пропозициональная переменная, означающая, что голубь i сидит в отверстии j . Для каждого i ∈ { 1 , … , n + 1 } и j ∈ { 0 , … , n } пусть$i \in \{1, \dotsc, n+1 \}$$j \in \{1, \dotsc, n \}$$p_{i,j}$$i$$j$$i \in \{1, \dotsc, n+1 \}$$j \in \{0, \dotsc, n \}$$y_{i,j}$$3$${EP}_i$$i$

$${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}.$$ $3$${EPHP}_n^{n+1}$${EP}_i$$H_k^{i,j} \equiv \neg p_{i,k} \vee \neg p_{j,k}$$i,j \in \{1, \dotsc, n+1 \}, i \ne j$$k \in \{1, \dotsc, n \}$

$n$${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?