Algorithmes SAT non basés sur DPLL

Réponses:

21

La recherche de résolution (appliquer simplement la règle de résolution avec de bonnes heuristiques) est une autre stratégie possible pour les solveurs SAT. Théoriquement, il est exponentiellement plus puissant (c'est-à-dire qu'il existe des problèmes pour lesquels il a des preuves exponentielles plus courtes) que DPLL (qui ne fait que la résolution d'arbre bien que vous puissiez l'augmenter avec un apprentissage nogood pour augmenter sa puissance - si cela le rend aussi puissant que la résolution générale est toujours ouvert pour autant que je sache) mais je ne connais pas une implémentation réelle qui fonctionne mieux.

Si vous ne vous limitez pas à terminer la recherche, alors WalkSat est un solveur de recherche local qui peut être utilisé pour trouver des solutions satisfaisantes et surpasse la recherche basée sur DPLL dans de nombreux cas. On ne peut pas l'utiliser pour prouver l'insatisfaisabilité, sauf si l'on met en cache toutes les affectations qui ont échoué, ce qui signifierait des besoins de mémoire exponentiels.

Edit: Oublié d'ajouter - Les plans de coupe peuvent également être utilisés (en réduisant SAT en un programme entier). En particulier, les coupes Gomory suffisent pour résoudre tout programme entier à l'optimalité. Dans le pire des cas, un nombre exponentiel peut être nécessaire. Je pense que le livre Arora & Barak's Computational Complexity contient quelques autres exemples de systèmes de preuve que l'on pourrait en théorie utiliser pour quelque chose comme la résolution SAT. Encore une fois, je n'ai pas vraiment vu une implémentation rapide de quoi que ce soit en dehors des méthodes basées sur DPLL ou basées sur la recherche locale.

Opter
la source
9
Il a été démontré que DPLL avec l'apprentissage de la clause (ou l'apprentissage nogood, comme vous l'appelez) et les redémarrages sont équivalents à la résolution générale.
Jan Johannsen
1
@JanJohannsen, est-ce le document auquel vous faites référence? arxiv.org/abs/1107.0044
Radu GRIGore
5
Oui, il y a aussi une amélioration dans l'article suivant: Knot Pipatsrisawat et Adnan Darwiche. Sur la puissance des solveurs SAT d'apprentissage des clauses comme moteurs de résolution. Artificial Intelligence 175 (2), 2011, p. 512-525. dx.doi.org/10.1016/j.artint.2010.10.002
Jan Johannsen
3
Alors que l'article de Beame et al. lié par Radu Grigore montre que la résolution générale est simulée p par un algorithme DPLL avec une stratégie d'apprentissage artificielle particulière, l'article ci-dessus le montre pour les stratégies d'apprentissage naturelles qui sont réellement utilisées.
Jan Johannsen
12

La propagation de l'enquête est un autre algorithme qui a été utilisé avec succès sur certains types de problèmes SAT, notamment les instances SAT aléatoires. Comme WalkSAT, il ne peut pas être utilisé pour prouver l'insatisfaction, mais il est basé sur des idées très différentes (algorithmes de transmission de messages) de WalkSAT.

Timothy Chow
la source
10

Il existe des solveurs SAT basés sur la recherche locale. Voir, par exemple, cet article pour une exposition.

ilyaraz
la source
7

Vous pouvez également dire que tous les solveurs CSP sont également des solveurs SAT. Et il y a autant que je sache deux méthodes utilisées dans CSP:

  • DFS exhaustif avec élagage de l'espace de recherche et vérification de la cohérence de l'arc, éventuellement en utilisant le rasage pour s'assurer que la cohérence est maintenue dès que possible.
  • Méthodes locales (recherche taboue, recuit simulé)
malejpavouk
la source
4

Monte Carlo Tree Search (MCTS) a récemment obtenu des résultats impressionnants sur des jeux tels que Go. L'idée de base approximative est d'entrelacer la simulation aléatoire avec la recherche d'arbre. Il est léger et facile à implémenter, la page du hub de recherche que j'ai liée contient de nombreux exemples, articles et du code.

Previti et al. [1] a effectué une enquête préliminaire sur les SCTM auprès de SAT. Ils appellent l'algorithme de recherche basé sur les SCTM UCTSAT ("limites de confiance supérieures appliquées aux arbres SAT", si vous voulez). Ils ont comparé les performances de DPLL et UCTSAT sur les instances du référentiel SATLIB, dans le but de voir si UCTSAT produirait des arbres de recherche beaucoup plus petits que DPLL.

Pour les instances de coloration uniformes aléatoires 3-SAT et graphes plats de différentes tailles, il n'y avait pas de différences significatives. Cependant, UCTSAT fonctionnait mieux pour les instances du monde réel. La taille moyenne des arbres (en termes de nombre de nœuds) pour quatre instances différentes d'analyse des défauts de circuit SSA était de plusieurs milliers pour DPLL, alors qu'elle était toujours inférieure à 200 pour UCTSAT.

[1] Previti, Alessandro, Raghuram Ramanujan, Marco Schaerf et Bart Selman. "Recherche UCT de style Monte-carlo pour la satisfiabilité booléenne." Dans AI * IA 2011: Intelligence artificielle autour de l'homme et au-delà, pp. 177-188. Springer Berlin Heidelberg, 2011.

Juho
la source
-4

DPLL ne spécifie pas strictement l'ordre des visites variables et il existe de nombreuses recherches intéressantes sur les stratégies d'attaque optimales par ordre variable. une partie de cela est incorporée dans la logique de sélection des variables dans les algorithmes SAT. en un sens, certaines de ces recherches sont préliminaires en ce qu'elles montrent que différents ordres d'attaque variables conduisent à différentes contraintes séquentielles (qui sont fortement corrélées à la dureté des instances), et la conception des heuristiques ou des stratégies les plus efficaces pour exploiter cet aperçu apparemment clé semble être dans les premiers stades de la recherche.

vzn
la source
4
Comprenez-vous que j'ai demandé des algorithmes non basés sur DPLL ?
Anonyme
2
Comprenez-vous ce que signifie «basé» ? Je vous l'ai dit : n'utilisez pas mes questions pour commenter ce que vous voulez commenter!
Anonyme
7
vous dites vous-même qu'ils sont basés sur DPLL. il me semble que cela revient à dire que différentes règles de pivot pour simplex vous donnent un algorithme qui n'est pas un algorithme simplex
Sasho Nikolov
7
Je suis d'accord avec Sasho. De plus, la recherche sur l'heuristique de l'ordre des variables n'en est certainement pas à ses débuts. L'importance a été prise en compte il y a longtemps (imaginez les conséquences d'un oracle parfait), et beaucoup de temps a été consacré à leur analyse. Les heuristiques d' ordre de valeur deviennent plus intéressantes dans les solveurs CSP, et pour une raison quelconque, je ne pense pas que la recherche sur eux ait été aussi florissante que pour l'ordre des variables.
Juho
4
Pour être plus précis, la recherche initiale sur l'heuristique de l'ordre des variables remonte aux années 70. Si vous êtes intéressé, je peux trouver les références pertinentes pour vous.
Juho