English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper considers the length of resolution proofs when usingKrishnamurthy's classic symmetry rules. We show that inconsistent linearequation systems of bounded width over a fixed finite field $\mathbb{F}_p$ with$p$ a prime have, in their standard encoding as CNFs, polynomial lengthresolutions when using the local symmetry rule (SRC-II).  As a consequence it follows that the multipede instances for the graphisomorphism problem encoded as CNF formula have polynomial length resolutionproofs. This contrasts exponential lower bounds forindividualization-refinement algorithms on these graphs.  For the Cai-F\"urer-Immerman graphs, for which Tor\'an showed exponentiallower bounds for resolution proofs (SAT 2013), we also show that already theglobal symmetry rule (SRC-I) suffices to allow for polynomial length proofs.

Resolution with Symmetry Rule applied to Linear Equations