Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the ... more >>>

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from ... more >>>

We consider the robustness of computational hardness of problems
whose input is obtained by applying independent random deletions to worst-case instances.
For some classical NP-hard problems on graphs, such as Coloring, Vertex-Cover, and Hamiltonicity, we examine the complexity of these problems when edges (or vertices) of an arbitrary
graph are ... more >>>