Comment savoir si un solveur SAT progresse dans sa tentative de réfuter une formule ? S’il a franchi une étape vers une réfutation ? Si la déduction qu’il vient de produire sera vraiment utile ? Si les déductions produites vont s’agréger de manière efficace ? Ces questions me hantent depuis des années, pour ne pas dire des décennies.

DPLL repave parcimonieusement l’espace des interprétations avec des dalles qui ne se chevauchent pas. CDCL, au contraire, produit des clauses pouvant être représentées par des dalles qui se chevauchent, ce qui rend difficile de décider lesquelles conserver lorsque le nombre de clauses apprises commence à ralentir sérieusement le solveur. Mais CDCL peut réfuter en temps polynomial certaines formules, telles que celles de type pebbling, qui ne peuvent être réfutées qu’en temps exponentiel par DPLL.

DPLL+R, la version de DPLL avec redémarrage et apprentissage des clauses représentant les connaissances déduites depuis le redémarrage précédent, a potentiellement la même puissance de déduction que CDCL. Mais comment guider les hypothèses (décisions) pour exploiter pleinement ce potentiel ?

Dans ce rapport, Je propose une politique de choix d’hypothèses pour DPLL+R qui permet de résoudre les formules pebbling en temps polynomial en construisant une réfutation se décomposant en étapes produisant chacune une clause qui subsume au moins une clause existante, de sorte que la formule se simplifie progressivement jusqu’à ce que la clause vide soit produite. Cette stratégie n’est pas du tout spécifique à une classe d’instances particulière et il serait intéressant de l’expérimenter sur d’autres formules. Je travaille actuellement au développement d’un solveur SAT basé sur ce principe.