💻 computer science

A Non-CDCL SAT Solver with Early Conflict Detection: The Watched-Literal-Based CSFLOC Solver

Cet article introduit CSFLOC-WL, un solveur SAT non-CDCL qui accélère l'approche originale de comptage de clauses de pleine longueur guidée par compteur en intégrant la propagation de préfixe par littéraux surveillés et la détection de conflits précoces pour identifier efficacement les sauts de compteur, démontrant une performance compétitive sur des instances 3-SAT aléatoires malgré l'absence des mécanismes de mise en cache matures de son prédécesseur.

Auteurs originaux : Gábor Kusper (Eszterházy Károly Catholic University)

Publié 2026-08-26

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Gábor Kusper (Eszterházy Károly Catholic University)

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Dans le vaste paysage de l'informatique, il existe un casse-tête fondamental connu sous le nom de problème de satisfaisabilité. Imaginez une serrure complexe dotée de milliers de goupilles, chacune représentant une variable qui peut être réglée sur l'un des deux états possibles. L'objectif est de trouver une unique combinaison de réglages qui ouvre la serrure, en respectant une longue liste de règles dictant comment les goupilles doivent s'aligner. Si aucune telle combinaison n'existe, la serrure est définitivement bloquée. Ce problème est central pour tout, de la vérification de la sécurité des micropuces à la planification de la logistique pour le transport maritime mondial. Pendant des décennies, les outils les plus puissants pour résoudre ce casse-tête ont reposé sur une stratégie consistant à faire une supposition, à suivre les conséquences logiques de cette supposition et, lorsqu'une contradiction est trouvée, à apprendre de l'erreur pour l'éviter à l'avenir. Cette approche, appelée apprentissage piloté par les conflits, est devenue le moteur standard et hautement perfectionné des logiciels de résolution de problèmes modernes.

Cependant, tous les chemins à travers la forêt des possibilités ne nécessitent pas la même carte. Un chercheur explore une route entièrement différente. Au lieu de deviner et d'apprendre des erreurs, sa méthode traite le problème comme un comptage systématique. Il imagine chaque réglage possible des goupilles de la serrure comme une longue ligne de nombres binaires, comptant de zéro jusqu'au maximum. L'objectif est de prouver que chaque nombre de cette ligne est bloqué par au moins une règle, ce qui signifie qu'aucune solution n'existe. Le défi a toujours été que vérifier chaque nombre un par un est impossibles de par sa lenteur. Le chercheur devait trouver un moyen de sauter de gigantesques segments de la ligne à la fois, en sautant par-dessus des millions de combinaisons impossibles en une seule étape.

Dans ses derniers travaux, le chercheur a introduit une nouvelle version de son solveur, appelée CSFLOC-WL3, qui modifie la manière dont il trouve ces sauts massifs. L'idée centrale est de ne pas considérer les règles comme des barrières statiques, mais comme des guides actifs. Tandis que le solveur compte à travers les possibilités, il assigne des valeurs aux variables dans un ordre fixe, un peu comme si l'on remplissait un formulaire de haut en bas. À chaque étape, il vérifie si l'assignation partielle actuelle force une règle à devenir une exigence unique et inévitable. Si une règle est forcée d'être vraie ou fausse par les choix faits jusqu'à présent, le solveur peut immédiatement voir que le chemin actuel est bloqué. L'innovation réside dans la manière dont il suit ces règles. Il utilise une technique appelée « littéraux surveillés » (watched literals), ce qui revient à avoir un moniteur dédié pour les parties les plus critiques de chaque règle. Ces moniteurs n'alertent le solveur que lorsqu'une règle est sur le point de devenir critique, permettant au système d'ignorer des milliers de vérifications non pertinentes et de se concentrer uniquement sur les moments où une décision compte.

La découverte la plus significative de cette nouvelle approche est un mécanisme permettant de détecter les conflits précocement. Dans l'ancienne méthode, le solveur pouvait marcher jusqu'à la fin d'une longue chaîne de logique avant de réaliser qu'il avait heurté une contradiction. Avec le nouveau système, si le chercheur constate que la même variable est forcée d'être à la fois vraie et fausse par deux règles différentes sous les mêmes conditions initiales, il s'arrête immédiatement. Il combine ensuite les raisons de ces deux forces opposées en une seule nouvelle règle. Cette nouvelle règle agit comme un puissant panneau indicateur, indiquant au solveur qu'il peut sauter non seulement le nombre actuel, mais aussi un bloc massif de nombres partageant le même motif de départ. Cela permet au solveur de franchir de vastes territoires de l'espace de recherche qui auraient pris beaucoup de temps à traverser un par un.

Le chercheur a testé ce nouveau solveur contre des concurrents établis sur une variété de problèmes difficiles et insolubles. Les résultats étaient révélateurs. Sur un ensemble de problèmes aléatoires et non structurés, le nouveau solveur était considérablement plus rapide, résolvant souvent en quelques secondes des instances qui prenaient des minutes ou qui échouaient complètement avec l'ancienne version. Dans ces cas, la capacité à détecter les conflits tôt et à faire de grands sauts s'est avérée décisive. Cependant, sur des problèmes plus structurés et complexes, le nouveau solveur était plus lent que son prédécesseur. La raison n'était pas un défaut de logique, mais un manque d'ingénierie. L'ancien solveur possédait un système de mémoire sophistiqué qui se souvenait des découvertes passées et les réutilisait, une fonctionnalité que la nouvelle version n'avait pas encore pleinement intégrée. Le nouveau solveur était excellent pour trouver de nouveaux chemins, mais il manquait de la bibliothèque de raccourcis passés dont disposait l'ancienne version.

Ce travail ne prétend pas avoir remplacé les méthodes standards utilisées par la plupart des ordinateurs aujourd'hui. Au lieu de cela, il démontre qu'une autre façon de concevoir le problème — basée sur un comptage systématique plutôt que sur la supposition et le retour en arrière (backtracking) — peut être très efficace lorsqu'elle est dotée des bons outils. L'étude montre qu'en empruntant une technique de suivi spécifique à l'approche dominante et en l'appliquant à cette méthode de comptage, il est possible de résoudre certains types de problèmes avec une rapidité remarquable. La voie à suivre est claire : en combinant la vitesse de détection précoce du nouveau système avec les systèmes de mémoire matures de l'ancienne génération, le chercheur pense pouvoir construire un solveur capable de répondre à un éventail plus large de défis. Ce travail est la preuve qu'il existe encore des territoires inexplorés dans la logique de l'informatique, et que parfois, la meilleure façon d'avancer est de changer entièrement la direction de la recherche.

Résumé Technique : Un solveur SAT non-CDCL avec détection de conflit précoce

Énoncé du problème
La satisfiabilité propositionnelle (SAT) est un problème de décision central en informatique. Alors que les solveurs de haute performance suivent principalement le paradigme de l'apprentissage de clauses par propagation de conflit (CDCL - Conflict-Driven Clause Learning), cet article étudie une approche alternative : le solveur CSFLOC. Le CSFLOC est une procédure de décision non-CDCL basée sur le comptage de clauses ordonnées de longueur complète subsumées. Le mécanisme central consiste à traverser l'espace ordonné des $2^n$ clauses de longueur complète (clauses contenant exactement un littéral pour chaque variable) à l'aide d'un compteur monotone. Si la clause de longueur complète actuelle n'est pas subsumée par la formule d'entrée, sa négation constitue une affectation satisfaisante. Si toutes les $2^n$ clauses sont subsumées, la formule est insatisfaisable.

Le goulot d'étranglement principal de l'implémentation originale de CSFLOC est la recherche répétée d'une clause subsumante pour la clause de longueur complète actuelle. Cette recherche nécessite de vérifier si une clause de la formule d'entrée est un sous-ensemble de la clause candidate actuelle. Bien que des améliorations d'ingénierie précédentes (telles que les observations du dernier bit positif et les caches de causes apprises) aient réduit le balayage, l'opération fondamentale restait un test de subsumption direct.

Méthodologie : CSFLOC-WL et détection de conflit précoce
L'article introduit CSFLOC-WL, une variante qui remplace la recherche explicite de subsumption par la propagation de préfixe par littéraux surveillés (watched-literal prefix propagation). Le solveur maintient la boucle du compteur global CSFLOC mais modifie la manière dont le prochain incrément du compteur (le saut) est découvert.

Propagation de préfixe par littéraux surveillés :
Au lieu de chercher une clause $D \subseteq C$ (où $C$ est la clause de longueur complète actuelle), le solveur assigne les variables selon la négation de $C$ (notée $\alpha$ ) dans un ordre fixe. Il utilise la structure de données standard des deux littéraux surveillés pour propager les conséquences unitaires sous cette assignation de préfixe.
- Une clause $D$ devient unitaire lorsque la propagation atteint l'indice de sa dernière variable ($last(D)$).
- Si la propagation dérive un littéral unitaire $u$ qui appartient à la clause de longueur complète $C$ actuelle, la clause de raison pour $u$ sert de cause de saut de compteur valide.
Détection de conflit précoce (ECD - Early Conflict Detection) :
L'innovation centrale est la détection de conflits avant que la propagation n'atteigne le niveau de la dernière variable. Si, sous un préfixe commun, la propagation dérive des conséquences unitaires opposées ( $x_i$ et $\bar{x}_i$ ) pour la même variable $x_i$ avec les clauses de raison $P$ et $N$ , le solveur résout immédiatement $P$ et $N$ sur $x_i$ .
- Théorème 1 (Détection de conflit précoce) : Le résolvant $D = Res_i(N, P)$ est entraî de la formule et est un sous-ensemble de la clause de longueur complète actuelle. Crucialement, si $D$ est non vide et non tautologique, l'indice de sa dernière variable est strictement inférieur à $i$ .
- Cela permet au compteur de sauter vers une limite déterminée par $last(D)$, permettant potentiellement de sauter un bloc plus important de l'espace de recherche que ne le permettrait l'attente que la propagation atteigne le niveau $i$ .
Architecture non-CDCL :
L'article souligne que CSFLOC-WL n'est pas un solveur CDCL. Il ne maintient pas d'arbre de décision, n'effectue pas de saut en arrière (backjumping) au sens du CDCL, et n'a pas de politique de redémarrage (restart). Le contrôle global reste un parcours monotone de l'espace des clauses de longueur complète. La structure des littéraux surveillés et la résolution sont utilisées strictement comme outils d'ingénierie pour découvrir des « causes de saut » (des clauses qui justifient de sauter des intervalles du compteur).

Contributions clés
L'article présente trois contributions spécifiques :

Formulation : Il reformule la recherche de subsumption de CSFLOC en une propagation de préfixe par littéraux surveillés sur la négation de la clause de longueur complète actuelle.
Preuve théorique : Il énonce et démontre le théorème de détection de conflit précoce, montrant que la résolution de conséquences unitaires opposées sous un préfixe commun produit une cause de saut de compteur valide qui peut permettre des sauts plus précoces que la recherche du dernier bit positif standard.
Implémentation et évaluation : Il présente CSFLOC-WL3, un prototype d'implémentation en Java, et le compare à :
- CSFLOC21TU : Une implémentation CSFLOC mature, orientée cache (sans littéraux surveillés).
- CaDiCaL 3.0.0 : Un solveur CDCL de pointe.
  L'évaluation inclut des instances UNSAT sélectionnées de SATLIB (3-SAT aléatoire, problème des chaises musicales, Dubois, ssa, etc.).

Résultats expérimentaux
Les expériences sur des instances sélectionnées de SATLIB (UNSAT) donnent des résultats mitigés, soulignant à la fois le potentiel et les limites actuelles de l'approche :

3-SAT aléatoire (famille uuf) : CSFLOC-WL3 démontre une force significative sur les instances aléatoires proches du seuil de satisfaisabilité. Sur des instances comme uuf150-01, uuf175-01 et uuf200-01, CSFLOC-WL3 est nettement plus rapide que CSFLOC21TU (qui expire sur les instances plus grandes) et compétitif ou plus rapide que CaDiCaL. Les statistiques internes montrent que CSFLOC-WL3 réduit le nombre d'itérations de la boucle principale de plusieurs ordres de grandeur (par exemple, de ~164 000 à ~1 200 sur uuf100-01) grâce aux grands sauts générés par la détection de conflit précoce.
Instances structurées : Sur les benchmarks structurés (pigeonhole, Dubois, ssa, bf), CSFLOC21TU surpasse généralement CSFLOC-WL3. L'article attribue cela au cache de causes apprises mature de CSFLOC21TU, qui réutilise efficacement les causes dérivées. CSFLOC-WL3 manque actuellement d'un mécanisme de mise en cache équivalent ; sa dépendance aux causes actives et au surcoût de la propagation le rend plus lent lorsque la propagation de préfixe ne génère pas de sauts suffisamment importants.
Comparaison avec CaDiCaL : CaDiCaL reste plus rapide sur la plupart des instances structurées. CSFLOC-WL3 n'est pas présenté comme un remplacement général des solveurs CDCL, mais comme une famille alternative viable qui rivalise bien sur certaines instances de 3-SAT aléatoires.

Signification et revendications
L'article affirme modestement que CSFLOC-WL3 est une étape dans le développement d'une nouvelle famille de solveurs, et non un remplacement du CDCL. Sa signification réside dans le fait que :

Il démontre que la propagation par littéraux surveillés et la détection de conflit précoce peuvent être adaptées efficacement à un cadre de comptage de clauses de longueur complète guidé par un compteur.
Il montre que cette approche peut surpasser les méthodes non-CDCL précédentes (CSFLOC21TU) et même les solveurs CDCL sur des instances spécifiques de 3-SAT aléatoire.
Il identifie une voie d'ingénierie claire : l'intégration d'un cache de causes apprises de type CSFLOC21TU dans l'implémentation à littéraux surveillés. L'auteur conclut que la combinaison de la puissance de génération de sauts de l'ECD avec l'efficacité de réutilisation d'un cache mature est la prochaine étape nécessaire pour rendre le solveur compétitif sur un éventail plus large de benchmarks.

L'article documente également deux nouvelles stratégies de renommage de variables, T (orientée préfixe two-SAT) et U (orientée unitaire), qui font partie de l'ingénierie actuelle mais ne sont pas l'objet principal de la contribution théorique.

Articles similaires