Proof complexity and the binary encoding of combinatorial principles

TL;DR

This paper investigates how binary encoding of combinatorial principles affects proof complexity across various refutation systems, contrasting it with traditional unary encoding methods.

Contribution

It introduces an analysis of proof complexity differences between binary and unary encodings in Resolution and Integer Linear Programming systems.

Findings

Binary encoding impacts proof complexity significantly.

Differences observed between unary and binary encodings in refutation systems.

Provides insights into encoding choices for proof complexity analysis.

Abstract

We consider Proof Complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this Proof Complexity with the normal unary encoding in several refutation systems, based on Resolution and Integer Linear Programming. Please consult the article for the full abstract.