Popular redundancy rules for SAT are not necessarily sound for MaxSAT. The works of [Bonacina-Bonet-Buss-Lauria’24] and [Ihalainen-Berg-Järvisalo’22] proposed ways to adapt them, but required specific encodings and more sophisticated checks during proof verification. Here, we propose a different way to adapt redundancy rules from SAT to MaxSAT. Our rules do not require specific encodings, their correctness is simpler to check, but they are slightly less expressive. However, the proposed redundancy rules, when added to MaxSAT-Resolution, are already strong enough to capture Branch-and-bound algorithms, enable short proofs of the optimal cost of notable principles (e.g., the Pigeonhole Principle and the Parity Principle), and allow to break simple symmetries (e.g., XOR-ification does not make formulas harder).

Ilario Bonacina: The author was supported by grant PID2022-138506NB-C22 (PROOFS BEYOND) funded by AEI. Maria Luisa Bonet: The author was supported by grant PID2022-138506NB-C22 (PROOFS BEYOND) funded by AEI. Massimo Lauria: The author has been supported by the project PRIN 2022 “Logical Methods in Combinatorics” N. 2022BXH4R5 of the Italian Ministry of University and Research (MIUR).

Peer Reviewed