Resolution with Symmetry Rule applied to Linear Equations

TL;DR

This paper demonstrates that applying symmetry rules in resolution proofs can significantly reduce proof length for certain linear systems and graph isomorphism problems, achieving polynomial bounds where exponential was previously known.

Contribution

It shows that symmetry rules enable polynomial length resolution proofs for bounded-width linear systems and specific graph isomorphism instances, contrasting prior exponential lower bounds.

Findings

Polynomial length resolution proofs for bounded-width linear systems over finite fields.

Polynomial proofs for multipede graph isomorphism instances using symmetry rules.

Symmetry rules reduce proof complexity for Cai-F"urer-Immerman graphs from exponential to polynomial.

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.