All reports by Author Ján Pich:

__
TR23-199
| 9th December 2023
__

Ján Pich, Rahul Santhanam#### Towards P $\neq$ NP from Extended Frege Lower Bounds

__
TR19-168
| 20th November 2019
__

Igor Carboni Oliveira, Lijie Chen, Shuichi Hirahara, Ján Pich, Ninad Rajgopal, Rahul Santhanam#### Beyond Natural Proofs: Hardness Magnification and Locality

__
TR18-158
| 11th September 2018
__

Igor Carboni Oliveira, Ján Pich, Rahul Santhanam#### Hardness magnification near state-of-the-art lower bounds

Revisions: 1

__
TR17-144
| 27th September 2017
__

Moritz Müller, Ján Pich#### Feasibly constructive proofs of succinct weak circuit lower bounds

Revisions: 1

__
TR17-044
| 21st February 2017
__

Olaf Beyersdorff, Luke Hinde, Ján Pich#### Reasons for Hardness in QBF Proof Systems

Revisions: 1

__
TR16-011
| 27th January 2016
__

Olaf Beyersdorff, Ján Pich#### Understanding Gentzen and Frege systems for QBF

__
TR13-077
| 14th May 2013
__

Ján Pich#### Circuit Lower Bounds in Bounded Arithmetics

__
TR10-046
| 22nd March 2010
__

Ján Pich#### Nisan-Wigderson generators in proof systems with forms of interpolation

Ján Pich, Rahul Santhanam

We give a new approach to the fundamental question of whether proof complexity lower bounds for concrete propositional proof systems imply super-polynomial Boolean circuit lower bounds.

For any poly-time computable function $f$, we define the witnessing formulas $w_n^k(f)$, which are propositional formulas stating that for any circuit $C$ of size ... more >>>

Igor Carboni Oliveira, Lijie Chen, Shuichi Hirahara, Ján Pich, Ninad Rajgopal, Rahul Santhanam

Hardness magnification reduces major complexity separations (such as $EXP \not\subseteq NC^1$) to proving lower bounds for some natural problem $Q$ against weak circuit models. Several recent works [OS18, MMW19, CT19, OPS19, CMMW19, Oli19, CJW19a] have established results of this form. In the most intriguing cases, the required lower bound is ... more >>>

Igor Carboni Oliveira, Ján Pich, Rahul Santhanam

This work continues the development of hardness magnification. The latter proposes a strategy for showing strong complexity lower bounds by reducing them to a refined analysis of weaker models, where combinatorial techniques might be successful.

We consider gap versions of the meta-computational problems MKtP and MCSP, where one needs ... more >>>

Moritz Müller, Ján Pich

We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length $n$. In 1995 Razborov showed that many can be proved in Cook’s theory $PV_1$, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small $n$ of ... more >>>

Olaf Beyersdorff, Luke Hinde, Ján Pich

We aim to understand inherent reasons for lower bounds for QBF proof systems and revisit and compare two previous approaches in this direction.

The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via strategy extraction (Beyersdorff & Pich, LICS'16). Here we ... more >>>

Olaf Beyersdorff, Ján Pich

Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from Beyersdorff et al., denoted EF+$\forall$red, which is a ... more >>>

Ján Pich

We prove that $T_{NC^1}$, the true universal first-order theory in the language containing names for all uniform $NC^1$ algorithms, cannot prove that for sufficiently large $n$, SAT is not computable by circuits of size $n^{2kc}$ where $k\geq 1, c\geq 4$ unless each function $f\in SIZE(n^k)$ can be approximated by formulas ... more >>>

Ján Pich

We prove that the Nisan-Wigderson generators based on computationally hard functions and suitable matrices are hard for propositional proof systems that admit feasible interpolation.

more >>>