Stasys Jukna

We prove a general combinatorial lower bound on the

size of monotone circuits. The argument is different from

Razborov's method of approximation, and is based on Sipser's

notion of `finite limit' and Haken's `counting bottlenecks' idea.

We then apply this criterion to the ...
more >>>

Stasys Jukna

We consider the minimal number of AND and OR gates in monotone

circuits for quadratic boolean functions, i.e. disjunctions of

length-$2$ monomials. The single level conjecture claims that

monotone single level circuits, i.e. circuits which have only one

level of AND gates, for quadratic functions ...
more >>>

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF ... more >>>

Pavel Hrubes, Pavel Pudlak

We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept that we call "unsatisfiability certificate". This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we ... 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 >>>