Name
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 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-Furer-Immerman graphs, for which Toran 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.4230/LIPIcs.STACS.2021.58 | 38TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS 2021) |
Keywords | DocType | Volume |
Logical Resolution, Symmetry Rule, Linear Equation System | Conference | 187 |
ISSN | Citations | PageRank |
1868-8969 | 0 | 0.34 |
References | Authors | |
0 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pascal Schweitzer | 1 | 34 | 6.39 |
| Constantin Seebach | 2 | 0 | 0.34 |