DRMaxSAT with MaxHS: first contact

Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva, Sam Buss

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

7 Citations (Scopus)


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. MaxHS-like algorithms, are as effective, and often more effective, than core-guided 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 MaxHS-like algorithm.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2019
Subtitle of host publication22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings
EditorsMikoláš Janota, Inês Lynce
Place of PublicationCham Switzerland
Number of pages11
ISBN (Electronic)9783030242589
ISBN (Print)9783030242572
Publication statusPublished - 2019
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2019 - Lisbon, Portugal
Duration: 7 Jul 201912 Jul 2019
Conference number: 22nd

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2019
Abbreviated titleSAT 2019
Internet address

Cite this