The concept of redundancy in SAT lead to more expressive and powerful proof search techniques, e.g. able to express various inprocessing techniques, and to interesting hierarchies of proof systems [Heule et.al’20, Buss-Thapen’19].
We propose a general way to integrate redundancy rules in MaxSAT, that is we define MaxSAT variants of ... more >>>