Y a-t-il eu des recherches sur -SAT au-dessus du seuil de satisfiabilité?

Une caractéristique bien connue des instances -SAT est le rapport du nombre de clauses sur le nombre de variables n , c'est-à-dire le quotient \ rho = m / n . Pour chaque k , il existe une valeur seuil \ alpha st \ pour \ rho \ ll \ alpha , la plupart des instances sont satisfaisables et pour \ rho \ gg \ alpha la plupart des instances ne sont pas satisfaisantes. Il y a eu beaucoup de recherches pour les problèmes où \ rho \ ll \ alpha , et pour les problèmes avec suffisamment petit \ rho , km n ρ = m / n k α ρ ≪ α ρ ≫ α ρ ≪ α ρ $k$$m$$n$$\rho = m/n$$k$$\alpha$$\rho \ll \alpha$$\rho \gg \alpha$$\rho \ll \alpha$$\rho$$k$-SAT devient soluble dans le temps polynomial. Voir, par exemple, l'article d'enquête de Dimitris Achlioptas tiré du Handbook of Satisfiability ( PDF ).

Je me demande si des travaux ont été effectués dans l'autre sens (où $\rho \gg \alpha$ ), par exemple, si nous pouvons en quelque sorte transformer le problème de CNF en DNF dans ce cas pour le résoudre rapidement.

Donc, essentiellement, que sait-on de SAT où $\rho = m/n \gg \alpha$ ?

Oui, il y en a eu. Moshe Vardi a récemment donné une conférence d'enquête lors de l'atelier sur les fondements théoriques de la résolution SAT appliquée de BIRS :

• Moshe Vardi, Transitions de phase et complexité informatique , 2014.

(Moshe présente le graphique de leur expérience un peu après la minute 14:30 dans son exposé lié ci-dessus.)

Soit le rapport de clause. À mesure que la valeur de augmente au-delà du seuil, le problème devient plus facile pour les solveurs SAT existants, mais pas aussi facile qu'avant d'atteindre le seuil. Il y a une très forte augmentation de la difficulté lorsque nous approchons du seuil par le bas. Après le seuil, le problème devient plus facile par rapport au seuil mais la diminution de difficulté est beaucoup moins forte.$\rho$$\rho$

Soit la difficulté du problème par rapport à (dans leur expérience est le temps d'exécution médian de GRASP sur des instances 3SAT aléatoires avec le rapport de clause ). Moshe suggère que change comme suit:$T_\rho(n)$$n$$T_\rho(n)$$\rho$$T_\rho(n)$

• $\rho \ll$ le seuil: est polynomial en ,$T_\rho(n)$$n$
• $\rho$ est proche du seuil: est exponentiel en ,$T_\rho(n)$$n$
• $\rho \gg$ le seuil: reste exponentiel en mais l'exposant diminue à mesure que augmente.$T_\rho(n)$$n$$\rho$

Il existe au moins deux axes de recherche concernant les aléatoires pour les formules avec un rapport clause / variable supérieur au seuil de satisfiabilité:$k\text-\mathsf{SAT}$

• Pour de telles formules, des bornes inférieures sur la longueur des réfutations en résolution et des systèmes de preuve propositionnelle plus forts ont été montrés, en commençant par l'article " De nombreux exemples concrets de résolution " de Chvátal et Szemerédi. Ces limites inférieures de résolution impliquent des limites inférieures sur l'exécution des solveurs SAT basés sur DPLL et CDCL. Les limites inférieures les plus fortes sont pour le calcul polynomial, en raison de Ben-Sasson et Impagliazzo .
• Pour ces formules, il existe des algorithmes déterministes efficaces pour certifier l’insatisfaisabilité, c’est-à-dire des algorithmes qui produisent soit "UNSAT" soit "Don't Know", où la réponse "UNSAT" doit être correcte, et elle doit produire "UNSAT" sur formules peu satisfaisantes à forte probabilité. Les meilleurs résultats dans cette direction sont dus à Feige et Ofek .

voici une étude / un angle plus ancien mais pertinent par un expert de premier plan.

• Le bord du couteau de contrainte Walsh 1998

$\kappa$

$\kappa$$\kappa$

$m/n \gg\alpha$