arXiv subjects

Erfan Khaniki

Publications and source records attributed to Erfan Khaniki.

5 recordsLinked to original sources

arXiv2026

The Proof Analysis Problem

Atserias and Müller (JACM, 2020) proved that for every unsatisfiable CNF formula $φ$, the formula $\operatorname{Ref}(φ)$, stating "$φ$ has small Resolution refutations", does not have subexponential-size Resolution refutations. Conversely, when $φ$ is satisfiable, Pudlák (TCS, 2003) showed how to construct a polynomial-size Resolution refutation of $\operatorname{Ref}(φ)$ given a satisfying assignment of $φ$. A question that remained open is: do all short Resolution refutations of $\operatorname{Ref}(φ)$ explicitly leak a satisfying assignment of $φ$? We answer this question affirmatively by giving a polynomial-time algorithm that extracts a satisfying assignment for $φ$ given any short Resolution refutation of $\operatorname{Ref}(φ)$. The algorithm follows from a new feasibly constructive proof of the Atserias-Müller lower bound, formalizable in Cook's theory $\mathsf{PV_1}$ of bounded arithmetic. Motivated by this, we introduce a computational problem concerning Resolution lower bounds: the Proof Analysis Problem (PAP). For a proof system $Q$, the Proof Analysis Problem for $Q$ asks, given a CNF formula $φ$ and a $Q$-proof of a Resolution lower bound for $φ$, encoded as $\neg \operatorname{Ref}(φ)$, whether $φ$ is satisfiable. In contrast to PAP for Resolution, we prove that PAP for Extended Frege (EF) is NP-complete. Our results yield new insights into proof complexity: (i) every proof system simulating EF is (weakly) automatable if and only if it is (weakly) automatable on formulas stating Resolution lower bounds; (ii) we provide Ref formulas exponentially hard for bounded-depth Frege systems; and (iii) for every strong enough theory of arithmetic $T$ we construct unsatisfiable CNF formulas exponentially hard for Resolution but for which $T$ cannot prove even a quadratic lower bound.

cs.CC↗

arXiv2024

From Proof Complexity to Circuit Complexity via Interactive Protocols

Folklore in complexity theory suspects that circuit lower bounds against $\mathbf{NC}^1$ or $\mathbf{P}/\operatorname{poly}$, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation $\mathbf{NEXP} \not\subseteq \mathbf{P}/\operatorname{poly}$, as recently observed by Pich and Santhanam (2023). We show such a connection conditionally for the Implicit Extended Frege proof system ($\mathsf{iEF}$) introduced by Krajíček (The Journal of Symbolic Logic, 2004), capable of formalizing most of contemporary complexity theory. In particular, we show that if $\mathsf{iEF}$ proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of $\mathsf{iEF}$ proofs implies $\#\mathbf{P} \not\subseteq \mathbf{FP}/\operatorname{poly}$ (which would in turn imply, for example, $\mathbf{PSPACE} \not\subseteq \mathbf{P}/\operatorname{poly}$). Our proof exploits the formalization inside $\mathsf{iEF}$ of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan (Journal of the ACM, 1992). This has consequences for the self-provability of circuit upper bounds in $\mathsf{iEF}$. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.

cs.CC↗

arXiv2022

The provably total recursive functions and the MRDP theorem in Basic Arithmetic and its extensions

We study Basic Arithmetic, BA introduced by W. Ruitenburg. BA is an arithmetical theory based on basic logic which is weaker than intuitionistic logic. We show that the class of the provably total recursive functions of BA is a proper sub-class of the primitive recursive functions. Three extensions of BA, called BA+U, BA_c and EBA are investigated with relation to their provably total recursive functions. It is shown that the provably total recursive functions of these three extensions of BA are exactly the primitive recursive functions. Moreover, among other things, it is shown that the well-known MRDP theorem does not hold in BA, BA+U, BA_c, but holds in EBA.

math.LO↗

arXiv2020

Not all Kripke models of $\sf HA$ are locally $\sf PA$

Let ${\bf K}$ be an arbitrary Kripke model of Heyting Arithmetic, ${\sf HA}$. For every node $k$ in ${\bf K}$, we can view the classical structure of $k$, ${\mathfrak M}_k$ as a model of some classical theory of arithmetic. Let ${\sf T}$ be a classical theory in the language of arithmetic. We say ${\bf K}$ is locally ${\sf T}$, iff for every $k$ in ${\bf K}$, ${\mathfrak M}_k\models{\sf T}$. One of the most important problems in the model theory of ${\sf HA}$ is the following question: {\it Is every Kripke model of ${\sf HA}$ locally ${\sf PA}$?} We answer this question negatively. We introduce two new Kripke model constructions to this end. The first construction actually characterizes the arithmetical structures that can be the root of a Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ (${\sf ECT_0}$ stands for Extended Church Thesis). The characterization says that for every arithmetical structure ${\mathfrak M}$, there exists a rooted Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ with the root $r$ such that ${\mathfrak M}_r={\mathfrak M}$ iff ${\mathfrak M}\models{\bf Th}_{Π_2}({\sf PA})$. One of the consequences of this characterization is that there is a rooted Kripke model ${\bf K}\Vdash{\sf HA}+{\sf ECT_0}$ with the root $r$ such that ${\mathfrak M}_r\not\models{\bf I}Δ_1$ and hence ${\bf K}$ is not even locally ${\bf I}Δ_1$. The second Kripke model construction is an implicit way of doing the first construction which works for any reasonable consistent intuitionistic arithmetical theory ${\sf T}$ with a recursively enumerable set of axioms that has the existence property. We get a sufficient condition from this construction that describes when for an arithmetical structure ${\mathfrak M}$, there exists a rooted Kripke model ${\bf K}\Vdash {\sf T}$ with the root $r$ such that ${\mathfrak M}_r={\mathfrak M}$.

math.LO↗

arXiv2019

New relations and separations of conjectures about incompleteness in the finite domain

Our main results are in the following three sections: 1. We prove new relations between proof complexity conjectures that are discussed in \cite{pu18}. 2. We investigate the existence of p-optimal proof systems for $\mathsf{TAUT}$, assuming the collapse of $\cal C$ and $\sf N{\cal C}$ (the nondeterministic version of $\cal C$) for some new classes $\cal C$ and also prove new conditional independence results for strong theories, assuming nonexistence of p-optimal proof systems. 3. We construct two new oracles ${\cal V}$ and ${\cal W}$. These two oracles imply several new separations of proof complexity conjectures in relativized worlds. Among them, we prove that existence of a p-optimal proof system for $\mathsf{TAUT}$ and existence of a complete problem for $\mathsf{TFNP}$ are independent of each other in relativized worlds which was not known before.

math.LO↗