Cargando…
MaxSAT Resolution and Subcube Sums
We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
2020
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326548/ http://dx.doi.org/10.1007/978-3-030-51825-7_21 |
_version_ | 1783552368418226176 |
---|---|
author | Filmus, Yuval Mahajan, Meena Sood, Gaurav Vinyals, Marc |
author_facet | Filmus, Yuval Mahajan, Meena Sood, Gaurav Vinyals, Marc |
author_sort | Filmus, Yuval |
collection | PubMed |
description | We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new semialgebraic proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, is a special case of the Sherali–Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums. |
format | Online Article Text |
id | pubmed-7326548 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2020 |
record_format | MEDLINE/PubMed |
spelling | pubmed-73265482020-07-01 MaxSAT Resolution and Subcube Sums Filmus, Yuval Mahajan, Meena Sood, Gaurav Vinyals, Marc Theory and Applications of Satisfiability Testing – SAT 2020 Article We study the MaxRes rule in the context of certifying unsatisfiability. We show that it can be exponentially more powerful than tree-like resolution, and when augmented with weakening (the system MaxResW), p-simulates tree-like resolution. In devising a lower bound technique specific to MaxRes (and not merely inheriting lower bounds from Res), we define a new semialgebraic proof system called the SubCubeSums proof system. This system, which p-simulates MaxResW, is a special case of the Sherali–Adams proof system. In expressivity, it is the integral restriction of conical juntas studied in the contexts of communication complexity and extension complexity. We show that it is not simulated by Res. Using a proof technique qualitatively different from the lower bounds that MaxResW inherits from Res, we show that Tseitin contradictions on expander graphs are hard to refute in SubCubeSums. We also establish a lower bound technique via lifting: for formulas requiring large degree in SubCubeSums, their XOR-ification requires large size in SubCubeSums. 2020-06-26 /pmc/articles/PMC7326548/ http://dx.doi.org/10.1007/978-3-030-51825-7_21 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic. |
spellingShingle | Article Filmus, Yuval Mahajan, Meena Sood, Gaurav Vinyals, Marc MaxSAT Resolution and Subcube Sums |
title | MaxSAT Resolution and Subcube Sums |
title_full | MaxSAT Resolution and Subcube Sums |
title_fullStr | MaxSAT Resolution and Subcube Sums |
title_full_unstemmed | MaxSAT Resolution and Subcube Sums |
title_short | MaxSAT Resolution and Subcube Sums |
title_sort | maxsat resolution and subcube sums |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326548/ http://dx.doi.org/10.1007/978-3-030-51825-7_21 |
work_keys_str_mv | AT filmusyuval maxsatresolutionandsubcubesums AT mahajanmeena maxsatresolutionandsubcubesums AT soodgaurav maxsatresolutionandsubcubesums AT vinyalsmarc maxsatresolutionandsubcubesums |