Previous Talks


[slides]
Date: Monday, February 21st, 2022 @ 1PM EST
Talk Title: Extremely Deep Proofs
Abstract: Recently, a number of works have observed an exceptionally strong type of tradeoff — known as a supercritical tradeoff — between resources in proof complexity, in which one parameter is pushed beyond worst-case when another is restricted. In this talk, I will describe how to obtain the first supercritical tradeoff (for resolution, k-DNF resolution, and Cutting Planes) between two natural parameters of proofs: size and depth. For the resolution proof system, size lower bounds show limitations of the runtime of modern CDCL solvers, while bounds on the depth imply that CDCL solvers are inherently sequential on these instances. Thus, this result can be seen as a very strong tradeoff between runtime and parallelizability. In describing how to prove this result, I will also sketch a simplified proof of a supercritical depth/width tradeoff due to Razborov. (Joint work with Robert Robere and Toniann Pitassi.)

Bio: Noah Fleming is a postdoctoral researcher at the University of California, San Diego. He received his PhD from the University of Toronto under the supervision of Toniann Pitassi. His research interests lie in the area of computational complexity with a particular focus on proof complexity and applications to algorithm design and analysis, circuit complexity, communication complexity, and property testing.


Date: Monday, January 17th, 2022 @ 1PM EST
Talk Title: The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability
Abstract: This disparity between theory and practice for SAT is believed to be a result of inherent properties of industrial SAT instances that make them tractable. Two characteristic properties seem to be prevalent in the majority of real-world SAT instances, heterogeneous degree distribution and locality. To understand the impact of these two properties on SAT, we study the proof complexity of random k-SAT models that allow to control heterogeneity and locality. Our findings show that heterogeneity alone does not make SAT easy as heterogeneous random k-SAT instances have superpolynomial resolution size. This implies intractability of these instances for modern SAT-solvers. On the other hand, modeling locality with an underlying geometry leads to small unsatisfiable subformulas, which can be found within polynomial time. A key ingredient for the result on geometric random k-SAT can be found in the complexity of higher-order Voronoi diagrams. As an additional technical contribution, we show an upper bound on the number of non-empty Voronoi regions, that holds for points with random positions in a very general setting. In particular, it covers arbitrary p-norms, higher dimensions, and weights affecting the area of influence of each point multiplicatively. Our bound is linear in the total weight. This is in stark contrast to quadratic lower bounds for the worst case.

Bio: Ralf Rothenberger is a PhD student studying computer science at the Hasso Plattner Institute in Potsdam, Germany, advised by Tobias Friedrich. He is researching random SAT and phase transitions. His interests also extend to proof complexity and connections to complex network models.


Date: Monday, December 13th, 2021 @ 1PM EST
Talk Title: Majority-3SAT (and Related Problems) in Polynomial Time
Abstract: Majority-SAT is the problem of determining whether an input n-variable formula in conjunctive normal form (CNF) has at least 2^(n-1) satisfying assignments. Majority-SAT and related problems have been studied extensively in various AI communities interested in the complexity of probabilistic planning and inference. Although Majority-SAT has been known to be PP-complete for over 40 years, the complexity of a natural variant has remained open: Majority-kSAT, where the input CNF formula is restricted to have clause width at most k. In recent work, joint with Ryan Williams, we prove that for every k, Majority-kSAT is in P. In fact, for any positive integer k and rational ρ in (0,1) with bounded denominator, we present an algorithm which determines whether a given k-CNF has at least ρ2^n satisfying assignments, in deterministic linear time (whereas the previous best-known algorithm ran in exponential time). In this talk we give an overview of the main ideas behind these algorithms, and highlight the implications for some additional problems related to counting satisfying assignments.

Bio: Shyan Akmal is a PhD student and Siebel scholar studying theoretical computer science at MIT, jointly advised by Virginia Vassilevska Williams and Ryan Williams. He performs research in fine-grained complexity and algorithm design. He is broadly interested in problems with connections to graph theory and combinatorics, and especially enjoys applications of algebraic methods in computer science.