Uma fórmula 3-CNF que requer largura de resolução

Recorde-se que a largura de uma resolução refutation de uma fórmula CNF M é o número máximo de literais em qualquer cláusula que ocorre em R . Para cada w , existem fórmulas insatisfatórias F no 3-CNF st. Cada refutação de resolução de F requer largura pelo menos w .$R$$F$$R$$w$$F$$F$$w$

Preciso de um exemplo concreto de uma fórmula insatisfatória no 3-CNF (tão pequena e simples quanto possível) que não tenha refutação de resolução da largura 4.

O exemplo a seguir vem do artigo que fornece uma caracterização combinatória da largura da resolução por Atserias e Dalmau ( Journal , ECCC , cópia do autor ).

O teorema 2 do artigo afirma que, dada a fórmula CNF , refutações de resolução de largura no máximo k para F são equivalentes a estratégias vencedoras para Spoiler no jogo de pedras existenciais ( k + 1 ) . Recorde-se que o jogo é jogado seixo existencial entre dois jogadores competem, chamados spoiler e duplicador, e as posições de jogo são atribuições parciais de tamanho de domínio no máximo k + 1 a variáveis de F . No jogo de pedras ( k + 1 ) , a partir da atribuição vazia, Spoiler deseja falsificar uma cláusula de $F$$k$$F$$(k+1)$$k+1$$F$$(k+1)$$F$enquanto se lembra de no máximo valores booleanos por vez, e o Duplicator quer impedir que o Spoiler o faça.$k+1$

O exemplo é baseado (na negação) no princípio do buraco de pombo.

$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}$${EPHP}_n^{n+1}$$n-1$

O artigo tem outro exemplo no Lema 9, baseado no princípio da ordem linear densa.

$\Omega(n^{(k-3)/12})$$k+1$