All reports by Author Neil Thapen:

__
TR24-001
| 2nd January 2024
__

Sam Buss, Neil Thapen#### A Simple Supercritical Tradeoff between Size and Height in Resolution

__
TR22-089
| 18th June 2022
__

Ilario Bonacina, Neil Thapen#### A separation of PLS from PPP

__
TR19-052
| 9th April 2019
__

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

__
TR16-175
| 8th November 2016
__

Pavel Pudlak, Neil Thapen#### Random resolution refutations

Revisions: 2

__
TR14-138
| 29th October 2014
__

Nicola Galesi, Pavel Pudlak, Neil Thapen#### The space complexity of cutting planes refutations

__
TR14-137
| 24th October 2014
__

Neil Thapen#### A trade-off between length and width in resolution

__
TR14-038
| 24th March 2014
__

Ilario Bonacina, Nicola Galesi, Neil Thapen#### Total space in resolution

Revisions: 1

__
TR13-149
| 28th October 2013
__

Albert Atserias, Neil Thapen#### The Ordering Principle in a Fragment of Approximate Counting

__
TR13-092
| 19th June 2013
__

Pavel Pudlak, Arnold Beckmann, Neil Thapen#### Parity Games and Propositional Proofs

Revisions: 1

__
TR13-038
| 13th March 2013
__

Massimo Lauria, Pavel Pudlak, Vojtech Rodl, Neil Thapen#### The complexity of proving that a graph is Ramsey

Revisions: 1

__
TR12-132
| 21st October 2012
__

Yuval Filmus, Massimo Lauria, Jakob NordstrÃ¶m, Noga Ron-Zewi, Neil Thapen#### Space Complexity in Polynomial Calculus

__
TR04-112
| 26th November 2004
__

Neil Thapen, Nicola Galesi#### Resolution and pebbling games

Sam Buss, Neil Thapen

We describe CNFs in n variables which, over a range of parameters, have small resolution refutations but are such that any small refutation must have height larger than n (even exponential in n), where the height of a refutation is the length of the longest path in it. This is ... more >>>

Ilario Bonacina, Neil Thapen

Recently it was shown that PLS is not contained in PPADS (ECCC report TR22-058). We show that this separation already implies that PLS is not contained in PPP. These separations are shown for the decision tree model of TFNP and imply similar separations in the type-2, relativized model.

Important note. ... 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 >>>

Pavel Pudlak, Neil Thapen

We study the \emph{random resolution} refutation system defined in~[Buss et al. 2014]. This attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. By proving the equivalence of several different definitions, we show that this concept is robust. On the ... more >>>

Nicola Galesi, Pavel Pudlak, Neil Thapen

We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of inequalities that need to be kept on a blackboard while verifying it. We show that any ... more >>>

Neil Thapen

We describe a family of CNF formulas in $n$ variables, with small initial width, which have polynomial length resolution refutations. By a result of Ben-Sasson and Wigderson it follows that they must also have narrow resolution refutations, of width $O(\sqrt {n \log n})$. We show that, for our formulas, this ... more >>>

Ilario Bonacina, Nicola Galesi, Neil Thapen

We show $\Omega(n^2)$ lower bounds on the total space used in resolution refutations of random $k$-CNFs over $n$ variables, and of the graph pigeonhole principle and the bit pigeonhole principle for $n$ holes. This answers the long-standing open problem of whether there are families of $k$-CNF formulas of size $O(n)$ ... more >>>

Albert Atserias, Neil Thapen

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over $\mathrm{T}^1_2$. This answers an open question raised in [Buss, Ko{\l}odziejczyk ... more >>>

Pavel Pudlak, Arnold Beckmann, Neil Thapen

A propositional proof system is \emph{weakly automatizable} if there

is a polynomial time algorithm which separates satisfiable formulas

from formulas which have a short refutation in the system, with

respect to a given length bound. We show that if the resolution

proof system is weakly automatizable, ...
more >>>

Massimo Lauria, Pavel Pudlak, Vojtech Rodl, Neil Thapen

We say that a graph with $n$ vertices is $c$-Ramsey if it does not contain either a clique or an independent set of size $c \log n$. We define a CNF formula which expresses this property for a graph $G$. We show a superpolynomial lower bound on the length of ... more >>>

Yuval Filmus, Massimo Lauria, Jakob NordstrÃ¶m, Noga Ron-Zewi, Neil Thapen

During the last decade, an active line of research in proof complexity has been to study space complexity and time-space trade-offs for proofs. Besides being a natural complexity measure of intrinsic interest, space is also an important issue in SAT solving, and so research has mostly focused on weak systems ... more >>>

Neil Thapen, Nicola Galesi

We define a collection of Prover-Delayer games that characterize certain subsystems of resolution. This allows us to give some natural criteria which guarantee lower bounds on the resolution width of a formula, and to extend these results to formulas of unbounded initial width.

We also use games to give upper ... more >>>