Article

    Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva and Sam Buss
    DRMaxSat with MaxHS: First Contact
    In: Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT 2019), 2019, pp. 239-249.

    Download preprint version.

Abstract: The proof system of Dual-Rail MaxSAT (DRMaxSAT) was recently shown to be capable of efficiently refuting families of formulas that are well-known to be hard for resolution, concretely when the MaxSAT solving approach is either MaxSAT resolution or core-guided algorithms. Moreover, DRMaxSAT based on MaxSAT resolution was shown to be stronger than general resolution. Nevertheless, existing experimental evidence indicates that the use of MaxSAT algorithms based on the computation of minimum hitting sets (MHSes), i.e. Max- HS-like algorithms, are as effective, and often more effective, than coreguided algorithms and algorithms based on MaxSAT resolution. This paper investigates the use of MaxHS-like algorithms in the DRMaxSAT proof system. Concretely, the paper proves that the propositional encoding of the pigenonhole and doubled pigenonhole principles have polynomial time refutations when the DRMaxSAT proof system uses a MaxHSlike algorithm.