Max-réfutations et oracles SAT

International audienceAdapter une réfutation par résolution en max-réfutation sans en augmenter considérablement sa taille est une question ouverte depuis l'introduction de la max-résolution. Cet article contribue à cette problématique en proposant un algorithme nommé algorithme de génération de remplaçants, capable d'adapter n'importe quelle réfutation par résolution en max-réfutation grâce à des appels à un oracle SAT. En particulier, on démontre que cet algorithme adapte efficacement les motifs en diamant, dont l'adaptation est exponentielle dans la littérature. Cet article résume le travail publié à la conférence ICTAI 2021 [3]