Un cas facile de SAT qui n'est pas facile pour la résolution d'arbre

Existe-t-il une classe naturelle de formules CNF - de préférence une qui a déjà été étudiée dans la littérature - avec les propriétés suivantes:$C$

• est un cas facile de SAT, comme par exemple Horn ou 2-CNF, c'est-à-dire que l'appartenance à C peut être testée en temps polynomial, et les formules F ∈ C peuvent être testées pour la satisfiabilité en temps polynomial.$C$$C$$F\in C$
• On ne sait pas que les formules non satisfaisantes ont des réfutations de résolution en forme d'arbre courtes (taille polynomiale). Encore mieux serait: il existe des formules insatisfaisantes en C pour lesquelles une borne inférieure super-polynomiale pour une résolution arborescente est connue.$F\in C$$C$
• D'un autre côté, les formules insatisfaisantes en sont connues pour avoir des preuves courtes dans un système de preuve plus fort, par exemple dans une résolution de type dag ou un système encore plus fort.$C$

ne devrait pas être trop rares,exemple, contiennentnombreuses formules avec n variables pour chaque (ou au moins pourplupartvaleurs de) n ∈ N . Il doit également être non trivial, dans le sens de contenir des formules satisfaisables et non satisfaisantes.$C$$n$$n\in \mathbb{N}$

L'approche suivante pour résoudre une formule CNF arbitraire devrait être significative: trouver une affectation partielle α st la formule résiduelle F α est en C , puis appliquer l'algorithme de temps polynomial pour les formules en C à F α . Par conséquent, je voudrais d'autres réponses en plus des contraintes toutes différentes de la réponse actuellement acceptée, car je pense qu'il est rare qu'une formule arbitraire devienne une contrainte toutes différentes après l'application d'une restriction.$F$$\alpha$$F\alpha$$C$$C$$F\alpha$

On dirait que vous êtes intéressé par des contraintes toutes différentes (et votre dernière phrase est sur la bonne voie). Ce sont des exemples non triviaux du principe du pigeonnier, où le nombre de pigeons n'est pas nécessairement supérieur au nombre de trous, et en outre certains pigeons peuvent être exclus de certains des trous.

Des contraintes toutes différentes peuvent être décidées en faisant correspondre le temps polynomial d'ordre inférieur.

• Jean-Charles Régin, Un algorithme de filtrage des contraintes de différence dans les CSP , AAAI 1994, 362–367.
• DE Knuth et A. Raghunathan, Le problème des représentants compatibles , SIAM J. Discrete Math. 5 422–427, 1992. doi: 10.1137 / 0405033

Lorsque des contraintes toutes différentes sont exprimées (en utilisant l'un des nombreux encodages) en tant qu'instances SAT, l'apprentissage des clauses axées sur les conflits trouve généralement rapidement une solution si elle existe. Cependant, la résolution pure pour PHP doit construire un ensemble de clauses superpolynomialement grand pour montrer que l'instance n'est pas satisfaisante. Cette limite vaut clairement pour ce problème plus général. D'un autre côté, rappelons que le codage de PHP par Cook permet des réfutations à résolution étendue de taille polynomiale .

• SA Cook, Une courte preuve du principe du trou de pigeon en utilisant une résolution étendue , SIGACT News 8 28–32, 1976. doi: 10.1145 / 1008335.1008338

Un travail récent dans ce sens est le chapitre 5 de la thèse de Sergi Oliva , qui a constitué la base d'un article avec Alberto Atserias au CCC 2013.

Je suppose que vous connaissez le résultat classique de Cook, alors peut-être que vous vouliez restreindre la puissance du système d'épreuve dans votre troisième condition?

Je ne sais pas pourquoi on exigerait également des formules sat, mais il y a quelques articles sur la séparation entre la résolution générale et la résolution d'arbre, par exemple [1]. Il me semble que c'est ce que vous voulez.

[1] Ben-Sasson, Eli, Russell Impagliazzo et Avi Wigderson. "Séparation presque optimale de la résolution arborescente et générale." Combinatorica 24.4 (2004): 585-603.

Vous pouvez être intéressé par les formules SAT avec une petite "bande passante" ou "largeur d'arbre" (logarythmique). Ces formules sont récursivement partitionnables de telle manière que la frontière de communication entre les partitions est petite, et donc une approche de programmation dynamique énumérative peut être utilisée pour les résoudre. Le sujet était populaire dans les années 90. Une fois, j'ai compté exactement le nombre de cycles hamiltoniens dans un petit graphique de largeur d'arbre de 24 000 sommets, donc les problèmes #P avec une petite largeur d'arbre sont également résolubles. Bodlaender est une référence majeure.

cet article suivant semble proche de ce qui est demandé à certains égards (s'il ne convient pas, JJ peut peut-être expliquer pourquoi). la question veut exclure les instances PHP (pigeonhole) en raison de l'absence de deux formules vraies / fausses, mais (comme cité dans les autres réponses) PHP est l'un des générateurs de cas / instances les plus étudiés du côté théorique et a a toujours été un générateur pour les deux formules satisfiable / insatisfiable bien que les formules satisfiables soient moins soulignées / étudiées.

${^m_n}$$m$$n$$m>n$$m \leq n$

• La résolution de type arbre est superpolynomialement plus lente que la résolution de type DAG pour le principe du trou de pigeon (1999) par Kazuo Iwama, Shuichi Miyazaki

une autre approche consisterait à adopter un angle plus empirique et à générer simplement des instances aléatoires (probablement autour du point de transition 50% satisfaisant facile-difficile-facile) et à les filtrer en fonction des critères énoncés. il faudrait des implémentations de résolution d'arbre / résolution DAG ou de "systèmes plus forts".