English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/235440
logo share SHARE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE
Exportar a otros formatos:


Equivalence Between Systems Stronger Than Resolution

AuthorsBonet, Maria Luisa; Levy, Jordi CSIC ORCID
Issue Date3-Jul-2020
CitationBonet M.L., Levy J. (2020) Equivalence Between Systems Stronger Than Resolution. In: Pulina L., Seidl M. (eds) Theory and Applications of Satisfiability Testing – SAT 2020. SAT 2020. Lecture Notes in Computer Science, vol 12178. Springer, Cham.
AbstractIn recent years there has been an increasing interest in studying proof systems stronger than Resolution, with the aim of building more efficient SAT solvers based on them. In defining these proof systems, we try to find a balance between the power of the proof system (the size of the proofs required to refute a formula) and the difficulty of finding the proofs. Among those proof systems we can mention Circular Resolution, MaxSAT Resolution with Extensions and MaxSAT Resolution with the Dual-Rail encoding. In this paper we study the relative power of those proof systems from a theoretical perspective. We prove that Circular Resolution and MaxSAT Resolution with extension are polynomially equivalent proof systems. This result is generalized to arbitrary sets of inference rules with proof constructions based on circular graphs or based on weighted clauses. We also prove that when we restrict the Split rule (that both systems use) to bounded size clauses, these two restricted systems are also equivalent. Finally, we show the relationship between these two restricted systems and Dual-Rail MaxSAT Resolution.
Publisher version (URL)http://dx.doi.org/10.1007/978-3-030-51825-7_13
Identifiersdoi: 10.1007/978-3-030-51825-7_13
isbn: 978-3-030-51824-0
Appears in Collections:(IIIA) Comunicaciones congresos
Files in This Item:
File Description SizeFormat 
Equivalence Between Systems Stronger Than Resolution.pdf551,88 kBUnknownView/Open
Show full item record
Review this work

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.