Ce qui fait tourner un solveur moderne
Ce que ce chapitre apporte
- Dire où passe réellement le temps dans un solveur, et le mesurer.
- Expliquer le mécanisme des deux littéraux surveillés et pourquoi il évite le travail au retour arrière.
- Décrire une heuristique de branchement fondée sur l'activité, et ce qu'elle exploite.
- Justifier l'intérêt des redémarrages malgré leur apparente absurdité.
- Expliquer pourquoi et comment un solveur oublie des clauses qu'il a apprises.
- Distinguer prétraitement et traitement en cours de recherche.
- Situer la résolution incrémentale et le parallélisme.
Où passe le temps
Toute l'ingénierie découle de ce chiffre. Optimiser l'analyse de conflit d'un facteur deux fait gagner quelques pour cent ; optimiser la propagation d'un facteur deux fait presque doubler la vitesse du solveur.
C'est pourquoi la structure de données de la propagation a été retravaillée pendant vingt ans, et pourquoi elle vient en premier dans ce chapitre.
Le code ci-dessous mesure le rapport, sur une instance aléatoire, avec le solveur du chapitre 7.
Sur cent clauses, cela passe. Sur un million, cela ne passe pas : chaque affectation coûterait un million d'examens, et il y a des millions d'affectations.
Il faut donc un mécanisme qui, à partir d'un littéral qui vient de devenir faux, désigne uniquement les clauses susceptibles de devenir unitaires. C'est l'objet de la section suivante.
Les deux littéraux surveillés
Dans chaque clause, on choisit deux littéraux, dits surveillés, qui ne sont pas faux.
Une clause n'a besoin d'être examinée que lorsque l'un de ses deux littéraux surveillés devient faux. Tant que les deux tiennent, la clause ne peut être ni unitaire ni falsifiée.
Surveiller deux littéraux non faux garantit donc exactement ce dont on a besoin : si les deux sont encore vivants, il reste au moins deux littéraux non faux dans la clause, donc rien à signaler.
Quand l'un des deux devient faux, il faut lui chercher un remplaçant parmi les autres littéraux. S'il en existe un, la clause redevient tranquille. S'il n'en existe pas, c'est que tous les autres sont faux : la clause est unitaire sur le littéral resté surveillé, ou falsifiée si celui-ci est faux aussi.
Soit , avec et surveillés.
| événement | ce que fait le solveur | surveillés |
|---|---|---|
| devient faux | rien, n'est pas surveillé | |
| devient faux | rien | |
| devient faux | cherche un remplaçant : n'est pas faux | |
| devient faux | cherche un remplaçant : , , sont tous faux | |
| la clause est unitaire, elle impose |
Deux événements sur quatre n'ont coûté strictement rien. Sur une clause de cent littéraux, ce serait quatre-vingt-dix-huit sur cent.
Quand le solveur défait des affectations, les littéraux surveillés d'une clause redeviennent non faux, puisqu'ils l'étaient déjà avant. Il n'y a donc rien à mettre à jour : la structure reste valide toute seule.
Or CDCL saute des niveaux entiers, des milliers de fois par seconde. Une structure qui exigerait de reparcourir les clauses à chaque retour arrière coûterait plus cher que tout le reste. Les deux littéraux surveillés sont la seule idée connue qui rende le retour arrière gratuit, et c'est ce qui a rendu CDCL praticable.
Ce qui compte est l'index inversé : pour chaque littéral, la liste des clauses qui le surveillent. Quand un littéral devient faux, le solveur va directement à cette liste, sans toucher aux autres clauses. C'est cet index qui remplace le parcours complet, et le choix des deux littéraux n'est qu'un moyen de le garder petit.
Choisir la variable : l'activité
À chaque variable est associé un compteur d'activité.
À chaque conflit, l'activité des variables qui apparaissent dans l'analyse est augmentée.
Périodiquement, toutes les activités sont divisées par une constante, ce qui fait décroître l'influence des conflits anciens.
Le solveur décide toujours de la variable libre la plus active.
La décroissance périodique est la moitié importante du mécanisme : elle fait oublier les conflits anciens, et concentre le solveur sur la région de l'espace où il se trouve maintenant. Sans elle, l'heuristique se figerait sur les premières variables rencontrées.
Le résultat est une recherche localisée : le solveur travaille longuement sur un petit groupe de variables liées entre elles, l'épuise, puis se déplace. C'est exactement ce qui convient aux instances industrielles, qui sont faites de communautés de variables fortement couplées.
L'idée paraît anodine et le gain est considérable. Après un retour arrière qui a défait cinquante affectations sans rapport avec le conflit, le solveur les retrouve immédiatement au lieu de les redécouvrir. Le travail perdu par un retour arrière profond est ainsi en grande partie récupéré.
Les redémarrages
Le solveur abandonne toutes ses décisions et revient au niveau 0, en conservant toutes les clauses apprises et toutes les activités.
Rien n'est perdu. Les clauses apprises restent, et elles feront propager immédiatement une bonne partie de ce qui avait été décidé. Ce que le redémarrage jette, ce sont les mauvais paris, pas les connaissances.
Il corrige les mauvais départs. Une recherche peut s'enfoncer dans une région sans issue à cause de trois décisions initiales malheureuses. Sans redémarrage, elle y reste des heures. Avec, elle reprend au niveau 0 avec une heuristique désormais informée par des milliers de conflits, et ne refera pas les mêmes premiers choix.
La suite de Luby : 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, … multipliée par un intervalle de base. Elle alterne redémarrages très fréquents et périodes longues, ce qui garantit de ne jamais rester bloqué trop longtemps quel que soit le comportement de l'instance. Elle a une justification théorique sur les algorithmes à temps d'exécution très variable.
Les redémarrages rapides, tous quelques centaines de conflits, éventuellement suspendus quand le solveur semble progresser. C'est la politique des solveurs orientés instances industrielles, où les redémarrages sont si fréquents que la recherche ressemble davantage à une exploration locale répétée qu'à un parcours.
Aucune des deux n'est meilleure partout, et les solveurs récents les combinent en choisissant selon des indicateurs mesurés en cours de route.
C'est un compromis entre deux paris opposés, et la suite de Luby a la propriété d'être, à un facteur logarithmique près, aussi bonne que la meilleure politique fixée à l'avance, sans rien savoir de l'instance.
Oublier des clauses
Un solveur qui apprend un million de clauses et les garde toutes propage si lentement qu'il perd plus qu'il ne gagne. Il faut donc oublier, régulièrement et massivement : les solveurs actuels suppriment souvent la moitié de leurs clauses apprises à chaque nettoyage.
Reste à choisir lesquelles, ce qui revient à prédire l'utilité future d'une clause qui n'a peut-être jamais servi.
Le LBD d'une clause, pour literal block distance, est le nombre de niveaux de décision distincts parmi ses littéraux.
Un LBD de 2 signifie que la clause relie seulement deux niveaux ; un LBD de 30 qu'elle en mêle trente.
Celles de LBD 2 sont si utiles qu'elles portent un nom, les clauses de colle : elles lient deux niveaux et propagent presque à chaque fois qu'on les rencontre. Les solveurs les gardent définitivement.
À l'inverse, une clause qui mêle trente niveaux décrit une coïncidence très particulière entre trente groupes de variables. Elle ne resservira sans doute jamais, et elle coûte à chaque propagation. C'est elle qu'il faut jeter.
Ce critère, publié en 2009, s'est révélé nettement meilleur que la longueur de la clause, qui semblait pourtant le choix naturel.
Simplifier la formule
Le prétraitement simplifie la formule une fois, avant de commencer.
Le traitement en cours de recherche applique les mêmes simplifications périodiquement, pendant la recherche, en profitant de ce que le solveur a appris entre-temps.
Subsomption. Jeter toute clause contenue dans une autre, au sens du chapitre 2. Les clauses apprises en produisent constamment.
Renforcement. Si et sont présentes, la seconde peut être raccourcie en . C'est une résolution qui produit une clause qui subsume l'un de ses parents.
Vivification. Prendre une clause apprise, tester ses littéraux un à un par propagation, et supprimer ceux dont on démontre qu'ils sont inutiles. Cher, mais très efficace sur les longues clauses.
Le prix est qu'il faut interrompre la recherche, et surtout que toute simplification doit rester traçable : le certificat DRAT du chapitre 6 doit enregistrer les suppressions comme les ajouts, sinon la preuve n'est plus vérifiable.
Résoudre plusieurs fois
Le solveur garde la formule et tout ce qu'il a appris en mémoire, et accepte une nouvelle question sous forme d'hypothèses : une liste de littéraux supposés vrais pour cette résolution seulement.
Sans incrémentalité, chacune de ces questions repart de zéro. Avec, le solveur conserve ses clauses apprises et ses activités : le premier appel est long, les suivants sont souvent des dizaines de fois plus rapides.
Et quand une résolution sous hypothèses échoue, le solveur rend le sous-ensemble des hypothèses responsable, ce qui est le noyau insatisfiable du chapitre 3, ciblé exactement sur la question posée.
Deux approches tiennent malgré tout. Le portefeuille lance plusieurs solveurs différemment réglés sur la même instance, qui s'échangent leurs meilleures clauses ; le gain vient de la diversité, pas du découpage. Le découpage en cubes partage l'espace de recherche en milliers de sous-problèmes traités indépendamment, et c'est ainsi qu'a été démontrée la conjecture de Pythagore booléenne mentionnée au chapitre 6.
Sur les instances ordinaires, le facteur d'accélération dépasse rarement deux ou trois, quel que soit le nombre de cœurs.
Ce que tout cela donne ensemble
Aucune de ces techniques ne change ce qui est calculé. La réponse est la même, le système de preuve est le même, les bornes du chapitre 6 sont les mêmes. Ce qui change est le coût constant de chaque opération élémentaire, et le nombre d'opérations inutiles évitées.
C'est le genre de progrès qu'on ne trouve pas en cherchant un meilleur algorithme, mais en mesurant obstinément où passe le temps. Trente ans de compétitions annuelles y ont plus contribué que n'importe quel théorème.
Exercices type
Pourquoi surveiller deux littéraux et non un seul ?
Avec un seul littéral surveillé, une clause devrait être examinée dès que ce littéral devient faux, sans savoir s'il en reste d'autres. Surtout, il faudrait vérifier après chaque affectation si la clause est devenue unitaire, ce qui ramène au parcours complet.
Avec deux, l'invariant est exactement celui qu'il faut : tant que les deux surveillés ne sont pas faux, la clause a au moins deux littéraux non faux, donc elle n'est ni unitaire ni falsifiée. Il n'y a rien à faire.
Trois littéraux surveillés donneraient un invariant plus fort, mais inutile : on veut détecter le passage à un littéral non faux, et deux suffisent pour cela.
Que faut-il mettre à jour dans les littéraux surveillés lors d'un retour arrière ?
Rien du tout, et c'est le point décisif.
Un littéral surveillé n'était pas faux avant le retour arrière, ou bien il avait été remplacé. Défaire des affectations ne peut que rendre des littéraux non faux : l'invariant reste donc vrai sans aucune intervention.
C'est ce qui rend le retour arrière non chronologique de CDCL utilisable. Une structure de données qui exigerait de reparcourir les clauses à chaque saut de niveau coûterait plus cher que tout ce qu'on aurait gagné.
Une clause apprise a un LBD de 2. Faut-il la garder ?
Oui, définitivement. C'est une clause de colle.
Un LBD de 2 signifie qu'elle ne relie que deux niveaux de décision, donc qu'elle exprime une contrainte très locale entre deux groupes de variables. Dès que l'un des deux niveaux est défait, la clause a de fortes chances de redevenir unitaire et de propager.
Ces clauses sont peu nombreuses et rendent d'énormes services. Les solveurs les excluent de tout nettoyage.
À l'inverse, une clause de LBD 30 mêle trente niveaux : elle décrit une coïncidence si particulière qu'elle ne resservira sans doute jamais, tout en coûtant à chaque propagation.
Un redémarrage fait-il perdre le travail accompli ?
Non, à l'exception des décisions elles-mêmes.
Ce qui est conservé : toutes les clauses apprises, toutes les activités des variables, et souvent la phase de chaque variable. Ce qui est jeté : la pile des décisions en cours.
Or au redémarrage, les clauses apprises propagent immédiatement une bonne partie de ce qui était affecté, sans qu'aucune décision soit nécessaire. Le solveur retrouve donc rapidement un état comparable, mais avec une heuristique mieux informée et sans les mauvais paris initiaux.
Un redémarrage jette des hypothèses, jamais des connaissances.
Pourquoi le parallélisme n'accélère-t-il pas un solveur d'un facteur égal au nombre de cœurs ?
Parce que la recherche est séquentielle par nature : chaque clause apprise change ce que le solveur fera ensuite. Deux cœurs qui explorent en parallèle ne se répartissent pas le travail, ils le dupliquent en grande partie.
Les deux réponses connues contournent le problème plutôt qu'elles ne le résolvent. Le portefeuille mise sur la diversité des réglages, et gagne quand l'un des solveurs a de la chance. Le découpage en cubes partage vraiment l'espace de recherche, mais demande de savoir le découper, ce qui n'est facile que sur certaines instances très structurées.
Sur une instance industrielle ordinaire, un facteur deux ou trois est un bon résultat, quel que soit le nombre de cœurs disponibles.
Le prétraitement change-t-il la réponse d'un solveur ?
Non, jamais la réponse. Mais il peut changer le modèle rendu, et cela demande une précaution.
L'élimination de variables produit une formule équisatisfiable, pas équivalente : les variables éliminées n'y figurent plus. Un modèle de la formule simplifiée n'est donc pas un modèle de la formule d'origine.
Le solveur doit conserver de quoi reconstruire les valeurs éliminées avant de rendre le modèle. C'est exactement le même problème qu'avec les variables de Tseitin au chapitre 2, et il se résout de la même façon : garder la trace de la transformation.
Une implémentation qui l'oublie rend des modèles incomplets ou faux, et c'est une source de bugs classique.
1.Sur une instance industrielle, un solveur passe l'essentiel de son temps à…
2.Une clause a deux littéraux surveillés, et un troisième littéral devient faux. Que fait le solveur ?
3.Que faut-il mettre à jour dans les littéraux surveillés au retour arrière ?
4.VSIDS choisit la variable…
5.Un redémarrage conserve…
6.Une clause apprise de LBD 2 est…
La méthode
- Mesurer avant d'optimiser : le rapport entre propagations et décisions dit où passe le temps.
- Ne jamais parcourir toutes les clauses à chaque affectation : passer par un index inversé.
- Surveiller deux littéraux non faux par clause, et ne rien faire tant qu'ils tiennent.
- Choisir la variable la plus impliquée dans les conflits récents, et faire décroître les activités.
- Redémarrer souvent, en conservant clauses apprises et activités.
- Oublier les clauses de fort LBD, garder définitivement celles de LBD 2.
- Simplifier pendant la recherche, pas seulement avant, et tracer toute suppression.
- Employer les hypothèses plutôt que relancer un solveur neuf à chaque variante.
Synthèse
- Un solveur passe 80 à 90 % de son temps à propager : c'est là qu'il faut optimiser.
- Les deux littéraux surveillés évitent d'examiner une clause tant qu'il lui reste deux littéraux non faux.
- Leur avantage décisif est que le retour arrière ne demande aucune mise à jour.
- VSIDS décide selon l'activité récente, avec une décroissance qui fait oublier les vieux conflits.
- La sauvegarde de phase récupère le travail perdu par un retour arrière profond.
- Un redémarrage jette les décisions, jamais les clauses apprises ni les activités.
- La suite de Luby alterne segments courts et longs, sans rien savoir de l'instance.
- Le LBD compte les niveaux distincts d'une clause ; celles de LBD 2 sont les clauses de colle.
- Élimination bornée, subsomption, renforcement et vivification s'appliquent pendant la recherche.
- La résolution incrémentale garde tout en mémoire et accepte des hypothèses : les appels suivants sont bien plus rapides.
- Le parallélisme apporte un facteur deux ou trois, pas davantage : la recherche est séquentielle par nature.
- Aucune de ces techniques ne change ce qui est calculé, seulement le coût de le calculer.