Страница публикации

DRMaxSAT with MaxHS: First Contact

Тип публикации: Статья в журнале

Тип материала: Текст

Авторы: Morgado A., Ignatiev A., Bonet M., Marques-Silva J., Buss S.

Журнал: Lecture Notes in Computer Science: Proc. of 22nd Intern. Conf. on Theory and Applications of Satisfiability Testing (SAT'2019; Lisbon; Portugal)

Язык публикации: english

Серия книг: Lecture Notes in Computer Science

Том: 11628

Номера страниц: 239-249

Количество страниц: 11

Год публикации: 2019

Отчетный год: 2019

DOI: 10.1007/978-3-030-24258-9_17

Аннотация: 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.

Индексируется WOS: Q4

Индексируется Scopus: Нет

Индексируется УБС: Нет

Индексируется РИНЦ: Да

Индексируется ВАК: Нет

Индексируется CORE: Нет