arXiv subjects

Neil Thapen

Publications and source records attributed to Neil Thapen.

11 recordsLinked to original sources

arXiv2026

Quantified propositional calculi and narrow implicit proofs

In the implicit version of a propositional proof system Q, we work with Q-proofs that are not written down directly, but are succinctly encoded by circuits. Thus implicit Q-proofs are potentially exponentially shorter than usual Q-proofs. We study narrow implicit proofs, a restricted version of this notion, in which lines in the encoded proof can only have polynomial size. We use a cut-elimination construction to show that G_{i+1} is equivalent to narrow implicit G_i, for i >= 1, where G_i is the extension of Frege allowing reasoning with Sigma^q_i quantified propositional formulas. We show that G_1 is equivalent to implicit resolution.

cs.LO↗

arXiv2025

On the consistency of stronger lower bounds for NEXP

It was recently shown by Atserias, Buss and Mueller that the standard complexity-theoretic conjecture NEXP not in P / poly is consistent with the relatively strong bounded arithmetic theory V^0_2, which can prove a substantial part of complexity theory. We observe that their approach can be extended to show that the stronger conjectures NEXP not in EXP / poly and NEXP not in coNEXP are consistent with a stronger theory, which includes every true universal number-sort sentence.

cs.LO↗

arXiv2024

How to fit large complexity classes into TFNP

Subclasses of TFNP (total functional NP) are usually defined by specifying a complete problem, which is necessarily in TFNP, and including all problems many-one reducible to it. We study two notions of how a TFNP problem can be reducible to an object, such as a complexity class, outside TFNP. This gives rise to subclasses of TFNP which capture some properties of that outside object. We show that well-known subclasses can arise in this way, for example PPA from reducibility to parity P and PLS from reducibility to P^NP. We study subclasses arising from PSPACE and the polynomial hierarchy, and show that they are characterized by the propositional proof systems Frege and constant-depth Frege, extending the known pairings between natural TFNP subclasses and proof systems. We study approximate counting from this point of view, and look for a subclass of TFNP that gives a natural home to combinatorial principles such as Ramsey which can be proved using approximate counting. We relate this to the recently-studied Long choice and Short choice problems.

cs.CC↗

arXiv2024

The strength of the dominance rule

It has become standard that, when a SAT solver decides that a CNF $\Gamma$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $\Gamma$ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) -- for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al.~2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system $G_1$, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER.

cs.LO↗

arXiv2022

Notes on switching lemmas

We prove three switching lemmas, for random restrictions for which variables are set independently; for random restrictions where variables are set in blocks (both due to Hastad [Hastad 86]); and for a distribution appropriate for the bijective pigeonhole principle [Beame et al. 94, Krajicek et al. 95]. The proofs are based on Beame's version [Beame 94] of Razborov's proof of the switching lemma in [Razborov 93], except using families of weighted restrictions rather than families of restrictions which are all the same size. This follows a suggestion of Beame in [Beame 94]. The result is something between Hastad's and Razborov's methods of proof. We use probabilistic arguments rather than counting ones, in a similar way to Hastad, but rather than doing induction on the terms in our formula with an inductive hypothesis involving conditional probability, as Hastad does, we explicitly build one function to bound the probabilities for the whole formula.

cs.CC↗

arXiv2021

First-Order Reasoning and Efficient Semi-Algebraic Proofs

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention recently due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP-hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds. This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones. We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule.

cs.LO↗

arXiv2019

DRAT and Propagation Redundancy Proofs Without New Variables

We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses $\Gamma$ derive the set of clauses $\Gamma \cup \{ C \}$ where, due to some syntactic condition, $\Gamma \cup \{ C \}$ is satisfiable if $\Gamma$ is, but where $\Gamma$ does not necessarily imply $C$. These inference rules include BC, RAT, SPR and PR (respectively short for blocked clauses, resolution asymmetric tautologies, subset propagation redundancy and propagation redundancy), which arose from work in satisfiability (SAT) solving. We introduce a new, more general rule SR (substitution redundancy). If the new clause $C$ is allowed to include new variables then the systems based on these rules are all equivalent to extended resolution. We focus on restricted systems that do not allow new variables. The systems with deletion, where we can delete a clause from our set at any time, are denoted DBC${}^-$, DRAT${}^-$, DSPR${}^-$, DPR${}^-$ and DSR${}^-$. The systems without deletion are BC${}^-$, RAT${}^-$, SPR${}^-$, PR${}^-$ and SR${}^-$. With deletion, we show that DRAT${}^-$, DSPR${}^-$ and DPR${}^-$ are equivalent. By earlier work of Kiesl, Rebola-Pardo and Heule, they are also equivalent to DBC${}^-$. Without deletion, we show that SPR${}^-$ can simulate PR${}^-$ provided only short clauses are inferred by SPR inferences. We also show that many of the well-known "hard" principles have small SPR${}^-$ refutations. These include the pigeonhole principle, bit pigeonhole principle, parity principle, Tseitin tautologies and clique-coloring tautologies. SPR${}^-$ can also handle or-fication and xor-ification, and lifting with an index gadget. Our final result is an exponential size lower bound for RAT${}^-$ refutations, giving exponential separations between RAT${}^-$ and both DRAT${}^-$ and SPR${}^-$.

cs.LO↗

arXiv2018

Approximate counting and NP search problems

We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory $\mathrm{APC}_2$ of [Je\v{r}\'abek 2009]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS. As CPLS is provably total in the theory $T^2_2$, this shows that $\mathrm{APC}_2$ does not prove every $\forall \Sigma^b_1$ sentence which is provable in bounded arithmetic. This answers the question posed in [Buss, Ko{\l}odziejczyk, Thapen 2014] and represents some progress in the programme of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences. Our main technical tool is an extension of the "fixing lemma" from [Pudl\'ak, Thapen 2017], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a $\textrm{P}^{\textrm{NP}}$ oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic.

math.LO↗

arXiv2014

How much randomness is needed for statistics?

In algorithmic randomness, when one wants to define a randomness notion with respect to some non-computable measure $λ$, a choice needs to be made. One approach is to allow randomness tests to access the measure $λ$ as an oracle (which we call the "classical approach"). The other approach is the opposite one, where the randomness tests are completely effective and do not have access to the information contained in $λ$ (we call this approach "Hippocratic"). While the Hippocratic approach is in general much more restrictive, there are cases where the two coincide. The first author showed in 2010 that in the particular case where the notion of randomness considered is Martin-Löf randomness and the measure $λ$ is a Bernoulli measure, classical randomness and Hippocratic randomness coincide. In this paper, we prove that this result no longer holds for other notions of randomness, namely computable randomness and stochasticity.

math.LO↗

arXiv2013

The complexity of proving that a graph is Ramsey

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 resolution proofs that $G$ is $c$-Ramsey, for every graph $G$. Our proof makes use of the fact that every Ramsey graph must contain a large subgraph with some of the statistical properties of the random graph.

cs.CC↗

arXiv2004

The strength of replacement in weak arithmetic

The replacement (or collection or choice) axiom scheme asserts bounded quantifier exchange. We prove the independence of this scheme from various weak theories of arithmetic, sometimes under a complexity assumption.

cs.LO↗