Mesurer la difficulté des instances SAT

28

Étant donné une instance de SAT, je voudrais pouvoir estimer à quel point il sera difficile de résoudre l'instance.

Une façon consiste à exécuter des solveurs existants, mais ce genre de résultat va à l'encontre du but d'estimer la difficulté. Une deuxième façon pourrait être de regarder le rapport des clauses aux variables, comme cela est fait pour les transitions de phase dans random-SAT, mais je suis sûr que de meilleures méthodes existent.

Étant donné une instance de SAT, existe-t-il des heuristiques rapides pour mesurer la difficulté? La seule condition est que ces heuristiques soient plus rapides que l'exécution de solveurs SAT existants sur l'instance.


Question connexe

Quels problèmes SAT sont faciles? sur cstheory.SE. Cette question porte sur des ensembles d'instances utilisables. C'est une question similaire, mais pas exactement la même. Je suis vraiment intéressé par une heuristique qui, étant donné une seule instance, fait une sorte de supposition semi-intelligente de savoir si l'instance sera difficile à résoudre.

Artem Kaznatcheev
la source
Pouvez-vous expliquer pourquoi la transition de phase par rapport à la "densité" n'est pas ce dont vous avez besoin?
Raphael
@Raphael, c'est une assez bonne méthode, et je le mentionne dans ma question. Mais j'ai eu l'impression qu'il existe encore de meilleures heuristiques. La transition de phase me dérange parce qu'elle semble si facile à tromper (il suffit d'ajouter des clauses ou une instance facilement satisfaisables à celle que vous essayez de déguiser)
Artem Kaznatcheev
Désolé, vous avez manqué cette partie de votre question. À droite, comme le notent les commentateurs, la transition de phase semble être sensible aux formules non aléatoires.
Raphael
2
Vous pouvez représenter une formule SAT (en CNF) sous forme de graphique bipartite, avec des sommets pour chaque formule et clause et des arêtes représentant des occurrences. Si ce graphique est facile à partitionner, le problème peut être décomposé en sous-graphiques partitionnés. Peut-être que cela peut servir de mesure utile? Je n'en ai aucune idée (c'est pourquoi il s'agit d'un commentaire et non d'une réponse).
Alex ten Brink
Vous pourriez trouver cela utile: ece.uwaterloo.ca/~vganesh/QPaper/paper.pdf
utilisateur

Réponses:

22

En général, c'est une question de recherche très pertinente et intéressante. "Une façon est d'exécuter les solveurs existants ..." et qu'est-ce que cela nous dirait même exactement? Nous pourrions voir empiriquement qu'une instance semble difficile pour un solveur spécifique ou un algorithme / heuristique spécifique, mais que dit-elle vraiment sur la dureté de l'instance?

Une voie qui a été poursuivie est l'identification de diverses propriétés structurelles des instances qui conduisent à des algorithmes efficaces. Ces propriétés sont en effet préférables à être "facilement" identifiables. Un exemple est la topologie du graphe de contraintes sous-jacent, mesurée à l'aide de divers paramètres de largeur de graphe. Par exemple, il est connu qu'une instance est résoluble en temps polynomial si la largeur d'arbre du graphe de contraintes sous-jacent est limitée par une constante.

Une autre approche s'est concentrée sur le rôle de la structure cachée des instances. Un exemple est l' ensemble de portes dérobées , c'est-à-dire l'ensemble de variables telles que lorsqu'elles sont instanciées, le problème restant se simplifie en une classe traitable. Par exemple, Williams et al., 2003 [1] montrent que même en tenant compte du coût de la recherche de variables de porte dérobée, on peut toujours obtenir un avantage de calcul global en se concentrant sur un ensemble de porte dérobée, à condition que l'ensemble soit suffisamment petit. De plus, Dilkina et al., 2007 [2] notent qu'un solveur appelé Satz-Rand est remarquablement bon pour trouver de petites portes dérobées solides sur une gamme de domaines expérimentaux.

Plus récemment, Ansotegui et al., 2008 [3] proposent l'utilisation de la complexité spatiale arborescente comme mesure pour les solveurs basés sur DPLL. Ils prouvent que l'espace à limites constantes implique également l'existence d'un algorithme de décision temporelle polynomiale, l'espace étant le degré du polynôme (Théorème 6 dans l'article). De plus, ils montrent que l'espace est plus petit que la taille des cycles-cutets. En fait, sous certaines hypothèses, l'espace est également plus petit que la taille des portes dérobées.

Ils officialisent également ce que je pense que vous recherchez, à savoir:

Trouvez une mesure , et un algorithme qui, étant donné une formule décide de la satisfiabilité dans le temps . Plus la mesure est petite, meilleure est la caractérisation de la dureté d'une formule .ψΓO(nψ(Γ))


[1] Williams, Ryan, Carla P. Gomes et Bart Selman. "Backdoors à la complexité typique de cas." Conférence conjointe internationale sur l'intelligence artificielle. Vol. 18, 2003.

[2] Dilkina, Bistra, Carla Gomes et Ashish Sabharwal. "Compromis dans la complexité de la détection de porte dérobée." Principes et pratique de la programmation par contraintes (CP 2007), pp. 256-270, 2007.

[3] Ansótegui, Carlos, Maria Luisa Bonet, Jordi Levy et Felip Manya. "Mesurer la dureté des instances SAT." Dans Actes de la 23e Conférence nationale sur l'intelligence artificielle (AAAI'08), pp. 222-228, 2008.

Juho
la source
J'aime la formalisation que vous citez. Il serait également intéressant de le raffiner pour indiquer explicitement que est efficacement calculable. Merci d'avoir répondu! Connaissez-vous des mesures moins formelles que les gens pourraient utiliser «en pratique»? ψ(Γ)
Artem Kaznatcheev
@ArtemKaznatcheev Je pense que l'ensemble de porte dérobée est probablement le seul vraiment utilisé. Lors de l'exécution d'un solveur, nous ne nous soucions pas vraiment de la dureté de la formule; l'instance doit néanmoins être résolue. La mesure doit nous donner un avantage de calcul, ou peut-être pouvons-nous l'utiliser pour choisir une heuristique appropriée. À part cela, je suppose que les mesures de dureté sont encore assez expérimentales.
Juho
1

Puisque vous connaissez la transition de phase, permettez-moi de mentionner quelques autres vérifications simples que je connais (qui sont probablement subsumées par l'analyse du graphe de contraintes):

  • Certains premiers générateurs SAT aléatoires ont créé par inadvertance des formules généralement faciles car ils utilisaient une «densité constante», ce qui signifie une proportion à peu près égale de toutes les longueurs de clause. Celles-ci étaient généralement faciles, car les clauses et les unités 2 simplifient considérablement le problème, comme il faut s'y attendre, et les clauses très longues n'ajoutent pas beaucoup de ramifications ou facilitent encore mieux l'hyper-résolution. Il semble donc préférable de s'en tenir aux clauses de longueur fixe et de faire varier d'autres paramètres.
  • De même, une règle de simplification puissante est l'élimination littérale pure. De toute évidence, une formule n'est vraiment aussi difficile que le nombre de littéraux impurs qu'elle possède. Parce que Resolution crée de nouvelles clauses numérotant(c'est-à-dire le produit des occurrences de et de sa négation), le nombre de résolvants est maximisé quand il y a un nombre égal de littéraux positifs et négatifs pour chaque variable. Par conséquent, les générateurs SAT équilibrés.|x||¬x|x
  • Il existe également une technique appelée "No Triangle SAT", qui semble assez récente [1], qui est une sorte de générateur d'instance dure qui interdit les "triangles". Un triangle est un ensemble de clauses contenant 3 variables qui se produisent par paire dans toutes les combinaisons dans un ensemble de clauses (c'est-à-dire ). Apparemment, les triangles ont tendance à rendre une formule plus facile pour les solveurs connus.v1,v2,v3{v1,v2,...},{v2,v3,...},{v1,v3,...}

[1] https://arxiv.org/pdf/1903.03592.pdf

Homme tondeuse
la source
0

En plus de l'excellente réponse de Juho, voici une autre approche:

Ercsey-Ravasz & Toroczkai, La dureté d'optimisation comme chaos transitoire dans une approche analogique de la satisfaction des contraintes , Nature Physics volume 7, pages 966–970 (2011).

Cette approche consiste à réécrire le problème SAT dans un système dynamique, où tout attracteur du système est une solution au problème SAT. Les bassins d'attraction du système sont plus fractals à mesure que le problème devient plus difficile, et donc la "difficulté" de l'instance SAT peut être mesurée en examinant à quel point les transitoires sont chaotiques avant la convergence du système.

En pratique, cela signifie démarrer un tas de solveurs à partir de différentes positions initiales et examiner la vitesse à laquelle les solveurs échappent aux transitoires chaotiques avant d'arriver à un attracteur.

Il n'est pas difficile de trouver un système dynamique pour lequel les "solutions" sont des solutions à un problème SAT donné, mais il est un peu plus difficile de s'assurer que les solutions sont toutes attractives et non répulsives. Leur solution est d'introduire des variables énergétiques (semblables aux multiplicateurs de Lagrange) pour représenter à quel point une contrainte est violée et d'essayer d'obtenir que le système minimise l'énergie du système.

Fait intéressant, en utilisant leur système dynamique, vous pouvez résoudre les problèmes SAT en temps polynomial sur un ordinateur analogique, ce qui en soi est un résultat remarquable. Il y a un hic; cela peut nécessiter des tensions exponentiellement grandes pour représenter les variables d'énergie, donc malheureusement vous ne pouvez pas le réaliser sur du matériel physique.

Pseudonyme
la source
1
"En utilisant leur système dynamique, vous pouvez résoudre les problèmes SAT en temps polynomial sur un ordinateur analogique, ce qui en soi est un résultat remarquable." Je ne suis pas d'accord pour dire que c'est remarquable. Comme vous le constatez: cela nécessite une précision exponentielle. Il s'agit en fait d'une astuce standard qui est directement liée à la définition de NP. Si vous pouviez mesurer une précision exponentielle, vous pourriez simplement essayer d'estimer le nombre de chemins d'acceptation (ou les voir comme des dyn sys de marche aléatoire) et voir si c'est exactement zéro ou quelques-uns (bien sûr, cela nécessiterait une mesure exponentiellement précise, comme avec le système dynamique).
Artem Kaznatcheev
Merci pour ça. Je ne connais pas beaucoup de résultats théoriques sur le calcul analogique.
Pseudonyme du