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

1 Citation (Scopus)

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. 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
PublisherSpringer
Pages239-249
Number of pages11
ISBN (Electronic)9783030242589
ISBN (Print)9783030242572
DOIs
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
http://sat2019.tecnico.ulisboa.pt/

Publication series

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

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2019
Abbreviated titleSAT 2019
CountryPortugal
CityLisbon
Period7/07/1912/07/19
Internet address

Cite this

Morgado, A., Ignatiev, A., Bonet, M. L., Marques-Silva, J., & Buss, S. (2019). DRMaxSAT with MaxHS: first contact. In M. Janota, & I. Lynce (Eds.), Theory and Applications of Satisfiability Testing – SAT 2019: 22nd International Conference, SAT 2019 Lisbon, Portugal, July 9–12, 2019 Proceedings (pp. 239-249). (Lecture Notes in Computer Science ; Vol. 11628 ). Springer. https://doi.org/10.1007/978-3-030-24258-9_17