We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.CC

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Computational Complexity

Title: Resolution with Symmetry Rule applied to Linear Equations

Authors: Pascal Schweitzer, Constantin Seebach (TU Kaiserslautern)
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 $\mathbb{F}_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\"urer-Immerman graphs, for which Tor\'an 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.
Comments: 18 pages, to be published in STACS 2021
Subjects: Computational Complexity (cs.CC); Discrete Mathematics (cs.DM)
ACM classes: F.2.2
Cite as: arXiv:2101.05142 [cs.CC]
  (or arXiv:2101.05142v1 [cs.CC] for this version)

Submission history

From: Constantin Seebach [view email]
[v1] Wed, 13 Jan 2021 15:37:11 GMT (24kb)

Link back to: arXiv, form interface, contact.