Certifying without loss of generality reasoning in solution-improving maximum satisfiability

Abstract

Dieter Vandesande tells that proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving

En Dieter Vandesande ens exposa que el registre de proves ha estat durant molt de temps el mètode establert per certificar la correcció dels solucionadors de satisfacció booleana (SAT), però fa poc que s'ha introduït per a l'optimització basada en SAT (MaxSAT). L'objectiu d'aquest article és la cerca de millora de solucions (SIS), en la qual es consulta iterativament un solucionador SAT per obtenir solucions cada cop més millors fins que se'n troba una d'òptima. Un aspecte desafiant dels solucionadors de SIS moderns és que fan ús d'arguments complexos "sense pèrdua de generalitat" que són força complicats per comprendre fins i tot a un meta-nivell humà, i molt menys per expressar-los en una prova simple i verificable per màquina. En aquest treball, desenvolupem mètodes de registre de proves pseudo-booleans per millorar la solució de MaxSAT i els fem servir per produir una versió de certificació del solucionador d'última generació Pacose amb proves de VeriPB. La nostra avaluació experimental demostra que aquest enfocament funciona a la pràctica. Esperem que aquest sigui un pas més cap a l'adopció general del registre de proves a la resolució de MaxSAT