Une restriction de la résolution étendue pour les démonstrateurs SAT modernes

National audienceLa plupart des solveurs SAT modernes se basent, avec succès, sur les mécanismes d'analyse de conflits et d'apprentissage initialement introduits dans les solveurs GRASP et CHAFF. D'un point de vue théorique, ce succès a été partiellement expliqué à l'aide de l'équivalence, en termes de puissance, entre le système de preuves implanté par l'apprentissage (avec redémarrages) et la résolution générale, alors que les précédents démonstrateurs SAT implantent des systèmes de preuve moins puissants. Néanmoins, des bornes inférieures exponentielles subsistent pour la résolution générale, ce qui suggère une voie prometteuse – mais théorique – permettant une amélioration significative des démonstrateurs SAT : l'utilisation de systèmes de preuves plus puissants. Transformer cette voie théorique en améliorations pratiques dans le cas général a cependant toujours échoué. Dans cet article, nous présentons un solveur SAT qui utilise une restriction de la résolution étendue. Ce solveur améliore les solveurs existant, en pratique, sur des instances issues des dernières compétitions, mais également sur des instances difficiles pour la résolution comme les instances XOR-SAT