All reports by Author Nicola Galesi:

__
TR19-069
| 6th May 2019
__

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova#### Bounded-depth Frege complexity of Tseitin formulas for all graphs

Revisions: 1

__
TR19-052
| 9th April 2019
__

Nicola Galesi, Leszek Kolodziejczyk, Neil Thapen#### Polynomial calculus space and resolution width

__
TR18-170
| 4th October 2018
__

Nicola Galesi, Navid Talebanfard, Jacobo Toran#### Cops-Robber games and the resolution of Tseitin formulas

__
TR18-165
| 20th September 2018
__

Stefan Dantchev, Nicola Galesi, Barnaby Martin#### Resolution and the binary encoding of combinatorial principles

Nicola Galesi, Dmitry Itsykson, Artur Riazanov, Anastasia Sofronova

We prove that there is a constant $K$ such that \emph{Tseitin} formulas for an undirected graph $G$ requires proofs of

size $2^{\mathrm{tw}(G)^{\Omega(1/d)}}$ in depth-$d$ Frege systems for $d<\frac{K \log n}{\log \log n}$, where $\tw(G)$ is the treewidth of $G$. This extends H{\aa}stad recent lower bound for the grid graph ...
more >>>

Nicola Galesi, Leszek Kolodziejczyk, Neil Thapen

We show that if a $k$-CNF requires width $w$ to refute in resolution, then it requires space $\sqrt w$ to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is ... more >>>

Nicola Galesi, Navid Talebanfard, Jacobo Toran

We characterize several complexity measures for the resolution of Tseitin formulas in terms of a two person cop-robber game. Our game is a slight variation of the one Seymour and Thomas used in order to characterize the tree-width parameter. For any undirected graph, by counting the number of cops needed ... more >>>

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 unusual binary} encoding. A motivation of our work is size lower bounds of refutations in Resolution for families of contradictions in ... more >>>