Ce récent article de FOCS2013, Strong Backdoors to Bounded Treewidth SAT par Gaspers et Szeider parle du lien entre la largeur d' arbre du graphe de la clause SAT et la dureté de l'instance.
Pour les instances 3-SAT aléatoires, c'est-à-dire les instances 3-SAT choisies au hasard, quelle est la corrélation entre la largeur d'arbre du graphe de clause et la dureté de l'instance?
La "dureté d'instance" peut être considérée comme "dure pour un solveur SAT typique", c'est-à-dire le temps de fonctionnement.
Je recherche des réponses ou des références de style théorique ou empirique. À ma connaissance, il ne semble pas y avoir d'études empiriques à ce sujet. Je suis conscient qu'il existe des façons quelque peu différentes de construire des graphiques de clause SAT, mais cette question n'est pas centrée sur la distinction.
Peut-être une question naturelle étroitement liée est de savoir comment la largeur d'arbre du graphe de clause est liée à la transition de phase 3-SAT.