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 >>>

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 >>>

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 >>>

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 >>>

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 >>>

The random $\Delta$-CNF model is one of the most important distribution over $\Delta\text{-}\mathrm{SAT}$ instances. It is closely connected to various areas of computer science, statistical physics, and is a benchmark for satisfiability algorithms. Fleming, Pankratov, Pitassi, and Robere and independently Hrubes and Pudlak showed that when $\Delta = \Theta(\log n)$, ... more >>>

In this paper, we study the problem of computing the majority function by low-depth monotone circuits and a related problem of constructing low-depth sorting networks. We consider both the classical setting with elementary operations of arity $2$ and the generalized setting with operations of arity $k$, where $k$ is a ... more >>>