Pourquoi y a-t-il une énorme différence entre les solveurs SAT?

Les solveurs SAT sont très importants dans les attaques algébriques , par exemple les marches et les minisat .

Cependant, lors de la résolution des problèmes de référence disponibles ici, il existe une énorme différence de performances entre les deux - Walksat est beaucoup plus rapide que minisat pour ces problèmes. Pourquoi est-ce?

Cette implémentation de walksat semble avoir quelques améliorations de performances - y a-t-il une raison pour laquelle elle n'a pas été incluse dans les compétitions internationales SAT ?

Oui, il existe une différence majeure entre MiniSAT et WalkSAT. Tout d'abord, clarifions - MiniSAT est une implémentation spécifique de la classe générique des algorithmes DPLL / CDCL qui utilise le retour en arrière et l'apprentissage des clauses, tandis que WalkSAT est le nom général d'un algorithme qui alterne entre les étapes gourmandes et les étapes aléatoires.

En général, DPLL / CDCL est beaucoup plus rapide sur les instances SAT structurées tandis que WalkSAT est plus rapide sur k-SAT aléatoire . Les instances SAT industrielles et appliquées ont tendance à avoir beaucoup de structure, donc DPLL / CDCL est dominant dans la plupart des solveurs SAT modernes. Cependant, une technique d'instance en instance peut être gagnante, ce qui explique pourquoi les solveurs de portefeuille sont devenus populaires.

Je prends beaucoup de problème avec votre affirmation selon laquelle WalkSAT est beaucoup plus rapide que MiniSAT sur les instances de cette page. D'une part, il y a des gigaoctets d'instances SAT - combien avez-vous essayé de les comparer? WalkSAT n'est pas du tout compétitif sur la plupart des instances structurées, c'est pourquoi il n'est pas souvent vu dans les compétitions.

Sur une note latérale - Vijay a raison que MiniSAT est toujours pertinent. En fait, parce qu'il est open source et bien écrit, MiniSAT est le solveur à battre pour montrer qu'une optimisation donnée est prometteuse. Beaucoup de gens modifient MiniSAT lui-même pour montrer leurs optimisations - jetez un œil à la catégorie "MiniSAT hack" dans les récentes compétitions SAT.

$A$$X$$Y$$B$$Y$$X$

Un bon article à lire sur ce sujet est celui de Nudelman et al . Le but de cet article est de déterminer les fonctionnalités faciles à calculer des instances SAT qui peuvent vous dire quels algorithmes sont susceptibles de bien fonctionner et lesquels ne le sont pas. En utilisant cette technique, il est possible de créer un algorithme basé sur un portefeuille qui analysera rapidement une instance de problème, puis résoudra l'instance avec l'algorithme le plus approprié. Il y a une progression des papiers qui suit celui-là; googler SATzilla va produire beaucoup de matériel de lecture.

$A$$B$