Une formule 3-CNF qui nécessite une largeur de résolution

Rappelons que la largeur d'une résolution réfutation $R$ d'une formule CNF $F$ est le nombre maximal de littéraux dans une clause se produisant dans $R$ . Pour chaque $w$ , il existe des formules insatisfaisantes $F$dans 3-CNF st chaque réfutation de résolution de $F$ nécessite une largeur d'au moins $w$ .

J'ai besoin d'un exemple concret d'une formule insatisfaisante en 3-CNF (aussi petite et simple que possible) qui n'a pas de réfutation de résolution de largeur 4.

L'exemple suivant provient de l'article qui donne une caractérisation combinatoire de la largeur de résolution par Atserias et Dalmau ( Journal , ECCC , copie de l'auteur ).

Le théorème 2 de l'article indique que, étant donné une formule CNF , les réfutations de résolution de largeur au plus k pour F sont équivalentes à des stratégies gagnantes pour Spoiler dans le jeu de galets existentiel ( k + 1 ) . Rappelons que le jeu de galets existentiel se joue entre deux joueurs en compétition, appelés Spoiler et Duplicator et les positions du jeu sont les affectations partielles de la taille de domaine au plus k + 1 à des variables de F . Dans le jeu ( k + 1 ) -pebble, à partir de l'affectation vide, Spoiler veut falsifier une clause de $F$$k$$F$$(k+1)$$k+1$$F$$(k+1)$$F$tout en se souvenant d'au plus valeurs booléennes à la fois, et Duplicator veut empêcher Spoiler de le faire.$k+1$

L'exemple est basé sur (la négation de) le principe du pigeonhole.

Pour chaque et j ∈ { 1 , … , n } , soit p i , j une variable propositionnelle signifiant que le pigeon i se trouve dans le trou j . Pour tout i ∈ { 1 , … , n + 1 } et j ∈ { 0 , … , n } , soit$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 \}$ soit une nouvelle variable propositionnelle. Laformule E P i 3 -CNF suivanteexprime que le pigeon i se trouve dans un trou: E P i ≡ ¬ y i , 0 ∧ n ⋀ j = 1 ( y i , j - 1 ∨ p i , j ∨ ¬ y i , j ) ∧ y i , 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}.$$ Enfin, la formule -CNF E P H P n + 1 n exprimant la négation du principe du pigeonhole est la conjonction de tout E P i et de toutes les clauses H i , j k ≡ ¬ p i , k ∨ ¬ p j , k pour i , j ∈ { 1 , … , n + 1 } , i ≠ j et$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 \}$

Le lemme 6 de l'article donne une preuve assez courte et intuitive que Spoiler ne peut pas gagner le jeu de cailloux sur E P H P n + 1 n , donc E P H P n + 1 n n'a pas de réfutation de résolution de largeur au plus n - 1 .$n$${EPHP}_n^{n+1}$${EPHP}_n^{n+1}$$n-1$

L'article a un autre exemple dans le lemme 9, basé sur le principe de l'ordre linéaire dense.

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