ABSTRACT. Recent decades have seen significant advances in the solution of computationally hard problems, in particular the decision problem for the NP-complete language SAT [Cook71]. Quantified Boolean formulas (QBF) extend propositional logic with existential and universal quantification, forming the prototypical PSPACE-complete language [StockmeyerM73]. Despite the higher complexity, QBF solvers are beginning to rival SAT solvers in certain application areas [FaymonvilleFRT17], and appear to be reaching the point of industrial applicability.

Alongside the development of solvers, there has been much interest in associated proof systems and their relative proof complexities [Buss12]. A host of QBF proof systems have been proposed, many of which extend some propositional system P to handle universal quantification [BeyersdorffCJ15]. A natural way to do this is to add a universal reduction rule, yielding the system P+$\forall$red [BeyersdorffBC16].

We present a new technique for proving proof-size lower bounds in P+$\forall$red. The technique relies only on two semantic measures: the cost of a QBF, and the capacity of a proof. Our central result, the Size-Cost-Capacity Theorem, states that proof-size in P+$\forall$red is at least the ratio of cost to capacity. By examining the capacity of proofs in several concrete systems (the universal reduction extensions of Resoution, Cutting Planes and Polynomial Calculus) we obtain lower bounds based solely on cost. Our technique provides genuine lower bounds in the sense that they continue to hold if P+$\forall$red is given access to an NP oracle [BeyersdorffHP17].

As applications of the technique, we first prove exponential lower bounds for the equality formulas, a new QBF family based on a simple two-player game. The main application is in proving exponential lower bounds with high probability for a class of randomly generated QBFs, the first genuine lower bounds of this kind. Finally, we employ the technique to give a simple proof of hardness for the prominent formulas of Kleine B\"{u}ning, Karpinski and Fl\"{o}gel [BuningKF95].

ABSTRACT. This work overviews recent results on the dual-rail based MaxSAT solving, including polynomial upper bounds on the refutation of PHP and 2PHP formulae with core-guided MaxSAT solvers and MaxSAT resolution as well as their relative efficiency compared to general resolution and cutting planes.

ABSTRACT. In this work, we extend a well-known connection between linear resolution refutation and read-once branching program by constructing proof systems based on syntactically restricted circuits studied in the field of Knowledge Compilation. While our approach only yield proof systems that are weaker than resolution, they may be used to define proof systems for problems such as #SAT or MaxSAT. This is a work in progress.

ABSTRACT. We examine the relationship between Q-Res and Exp+Res under the natural and practically important restriction to families of QBFs with bounded quantifier complexity. We show that (dag-like) Q-Res is p-simulated by Exp+Res in this case.

ABSTRACT. We propose arithmetic theories that link systems in monotone proof complexity to classes in monotone computational complexity. In particular, we focus on the case of polynomial-time, for which monotone function classes and monotone proof systems have recently been proposed. We complete the proof complexity theoretic account of this subject by proposing an accompanying logical theory, in the usual sense of 'bounded arithmetic'

ABSTRACT. Various key problems from theoretical computer science can be expressed as polynomial optimization problems over the boolean hypercube. One particularly successful way to prove complexity bounds for these types of problems are based on sums of squares (SOS) as nonnegativity certificates. In this article, we initiate optimization problems over the boolean hypercube via a recent, alternative certificate called sums of nonnegative circuit polynomials (SONC). We show that key results for SOS based certificates remain valid: First, for polynomials, which are nonnegative over the $n$-variate boolean hypercube with constraints of degree $d$ there exists a SONC certificate of degree at most $n+d$. Second, if there exists a degree $d$ SONC certificate for nonnegativity of a polynomial over the boolean hypercube, then there also exists a short degree $d$ SONC certificate, that includes at most $n^{O(d)}$ nonnegative circuit polynomials. Finally, we show certain differences between SOS and SONC cones namely, we prove, that in opposite to SOS, SONC cone is not closed under taking affine transformation of variables and that for SONC there does not exist an equivalent to Putinar's Positivestellensatz for SOS. We discuss these results both from algebraic and optimization perspective.

ABSTRACT. (in pdf)

ABSTRACT. We extend QBF resolution with a rule for exploiting symmetries and analyze the impact on the power of the new proof system.

ABSTRACT. It is well-known that there is an equivalence between ordered resolution and ordered binary decision diagrams (OBDD); i.e., for any unsatisfiable formula phi, the size of the smallest ordered resolution refutation of phi equal to the size of the smallest OBDD for the canonical search problem corresponding to phi. But there is no such equivalence between resolution and branching programs (BP).

In this project, we study different proof systems equivalent to classes of branching programs between BP and OBDD. These proof systems are similar to roABP-IPS, an algebraic proof system defined by Forbes et al. and based on the ideal proof system introduced by Grochow and Pitassi.

We show that proof systems equivalent to b-OBDD are not comparable with resolution and cutting planes (for b > 1). We also prove exponential lower bounds for these proof systems on Tseitin formulas. Additionally, we show that proof systems equivalent to (1,+b)-BP are strictly stronger than regular resolution for b > 0; moreover, resolution does not p-simulate (1, +b)-BP for b > 5.

ABSTRACT. One of the main successes in circuit complexity is the strong lower bounds on complexity of monotone circuits. By analogy, one might expect that studying monotone reasoning would lead to similar lower bounds in proof complexity. Yet surprisingly, Atserias, Galesi and Pudlak have given a general quasipolynomial simulation of sequent calculus LK by its monotone fragment MLK. Moreover, their techniques give a polynomial simulation, provided properties of AKS sorting networks can be formalized inside LK. Such formalization was obtained in 2011 by Jerabek, assuming provable in LK existence of expander graphs.

Several major results in complexity theory such as undirected graph reachability in logspace (Reingold, Rozenman-Vadhan) and monotone formulas for sorting (Ajtai-Komlos-Szemeredi sorting networks) are based on properties of expander graphs. But what is the complexity such proofs? Much of the existing expander constructions rely on computationally non-trivial algebraic concepts for the analysis, such as the spectral gap, even when constructions themselves are combinatorial.

In this work, we show that existence of expanders of arbitrary size can be proven using NC^1 reasoning. We give a fully combinatorial analysis of an iterative construction of expanders using replacement product, powering and tensoring, and formalize this analysis in the bounded arithmetic system VNC^1. Combined with Atserias, Galesi, Pudlak'2002 and Jerabek'2011, this completes the proof that monotone LK is as powerful as LK for proving monotone sequents.

Joint work with Sam Buss, Valentine Kabanets and Michal Koucky.

ABSTRACT. We give lower bounds in Resolution-with-bounded-conjunction, Res$(s)$, for families of contradictions where witnesses are given in the unusual binary encodings. The two families we focus on are the $k$-Clique Formulas and those associated with the (weak) Pigeonhole Principle. If one could give lower bounds in Res$(\log$) for such families under the binary encoding, then these would translate to lower bounds for the more typical unary encoding in Resolution, Res$(1)$. Such a lower bound is not possible for certain very weak Pigeonhole Principles, but might be dreamt of for the $k$-Clique Formulas.

ABSTRACT. We study the complexity of resolution extended with the ability to count over different characteristics and rings. These systems capture integer and moduli counting, and in particular admit short tree-like refutations for insolvable sets of linear equations. For this purpose, we consider the system ResLin(R), in which proof-lines are disjunction of linear equations over a ring R.(We focus on the case where the variables are Boolean, i.e., we add the Boolean axioms (x=0)\/(x=1), for all variables x.) Extending the work of Itsykson and Sokolov we obtain new lower bounds and separations, as follows:

Finite fields:

Exponential-size lower bounds for tree-like ResLin(Fp) refutations of Tseitin mod q formulas, for every pair of distinct primes p,q. As a corollary we obtain an exponential-size separation between tree-like ResLin(Fp) and tree-like ResLin(Fq).

Exponential-size lower bounds for tree-like ResLin(Fp) refutations of random k-CNF formulas, for every prime p and constant k.

Exponential-size lower bounds for tree-like ResLin(F) refutations of the pigeonhole principle, for every field F.

All the above hard instances are encoded as CNF formulas. The lower bounds are proved using extensions and modifications of the Prover-Delayer game technique and size-width relations.

Characteristic zero fields:

Separation of tree-like ResLin(F) and (dag-like) ResLin(F), for characteristic zero fields F. The separating instances are the pigeonhole principle and the Subset Sum principle. The latter is the formula a1 x1 +... +an xn = b, for some b not in the image of the linear form. The lower bound for the Subset Sum principle employs the notion of immunity from Alekhnovich and Razborov.