Computing Max-SAT Refutations using SAT Oracles
Matthieu Py, Mohamed Sami Cherif, Djamal Habet · 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI) · 2021
Adapting a resolution refutation for SAT into a Max-SAT resolution refutation without increasing considerably the size of the refutation is an open question. This paper contributes to this topic by introducing an algorithm, called substitute generation, able to adapt any resolution refutation to get a Max-SAT refutation using SAT oracles. This algorithm is able to efficiently adapt k-stacked diamond patterns, whose transformation is exponential in the literature.