Resolution and the binary encoding of combinatorial principles

Stefan Dantchev, Nicola Galesi, Barnaby Martin

We investigate the size complexity of proofs in $Res(s)$ -- an extension of Resolution working on $s$-DNFs instead of clauses -- for families of contradictions given in the {\em un…