License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2021.58
URN: urn:nbn:de:0030-drops-137038
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13703/
Schweitzer, Pascal ;
Seebach, Constantin
Resolution with Symmetry Rule Applied to Linear Equations
Abstract
This paper considers the length of resolution proofs when using Krishnamurthy’s classic symmetry rules. We show that inconsistent linear equation systems of bounded width over a fixed finite field ?_p with p a prime have, in their standard encoding as CNFs, polynomial length resolutions when using the local symmetry rule (SRC-II).
As a consequence it follows that the multipede instances for the graph isomorphism problem encoded as CNF formula have polynomial length resolution proofs. This contrasts exponential lower bounds for individualization-refinement algorithms on these graphs.
For the Cai-Fürer-Immerman graphs, for which Torán showed exponential lower bounds for resolution proofs (SAT 2013), we also show that already the global symmetry rule (SRC-I) suffices to allow for polynomial length proofs.
BibTeX - Entry
@InProceedings{schweitzer_et_al:LIPIcs.STACS.2021.58,
author = {Schweitzer, Pascal and Seebach, Constantin},
title = {{Resolution with Symmetry Rule Applied to Linear Equations}},
booktitle = {38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
pages = {58:1--58:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-180-1},
ISSN = {1868-8969},
year = {2021},
volume = {187},
editor = {Bl\"{a}ser, Markus and Monmege, Benjamin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13703},
URN = {urn:nbn:de:0030-drops-137038},
doi = {10.4230/LIPIcs.STACS.2021.58},
annote = {Keywords: Logical Resolution, Symmetry Rule, Linear Equation System}
}
Keywords: |
|
Logical Resolution, Symmetry Rule, Linear Equation System |
Collection: |
|
38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021) |
Issue Date: |
|
2021 |
Date of publication: |
|
10.03.2021 |