Guider la recherche CDCL SAT via l'exploration aléatoire en cas de dépression de conflit

Résumé

L'efficacité de la résolution de SAT par apprentissage des clauses en fonction des conflits (CDCL) dépend essentiellement de la rapidité avec laquelle les conflits sont trouvés. Les heuristiques de branchement CDCL les plus récentes, telles que VSIDS, CHB et LRB, répondent à cet objectif. Nous examinons de plus près la manière dont les conflits sont générés au cours d'une recherche SAT CDCL. Notre étude de l'heuristique de branchement VSIDS montre que les conflits sont typiquement générés en courtes rafales, suivies de ce que nous appelons une phase de dépression de conflit dans laquelle la recherche ne génère aucun conflit dans un intervalle de décisions. L'absence de conflit indique que les variables qui sont actuellement les mieux classées par l'heuristique de branchement ne génèrent pas de conflits. Sur la base de cette analyse, nous proposons une stratégie d'exploration, appelée expSAT, qui échantillonne aléatoirement des séquences de sélection de variables afin d'apprendre une heuristique mise à jour à partir des conflits générés. L'objectif est de sortir rapidement de la dépression des conflits. L'heuristique de branchement déployée dans expSAT combine ces mises à jour avec les scores d'activité VSIDS standard. Une évaluation empirique approfondie avec quatre solveurs SAT CDCL de pointe démontre que l'approche expSAT permet d'obtenir des gains de performance allant de bons à forts.