Proof Search and the Structure of Solution Spaces

In 2019, Moritz Müller and I resolved a longstanding open question on the computational complexity of proof search. The preliminary version of the article “Automating Resolution is NP-Hard” was the co-winner of the Best Paper Award at the 60th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2019). In its final version, the paper was invited for submission to the Journal of the ACM, and published in 2020 [1]. Why does the proof that yet another problem is NP-hard deserve such an important award? In this note I try to explain why. Let me begin with the historical background. This year is the 50th anniversary of Steve Cook’s article “The Complexity of Theorem Proving Procedures” [5]. Cook’s seminal work established that the satisfiability problem for propositional logic is NP-complete. For the first time, the generic task of searching a solution within an exponentially big space of candidate solutions was reduced to that of a concrete, well-defined, and combinatorially simple-to-state problem. The importance of Cook’s Theorem was quickly recognized. Only one year later, Richard Karp wrote another landmark paper where he established that “a large number of classic unsolved [computational] problems of covering, matching, packing, routing, assignment and sequencing are equivalent”. All of them, Karp showed, are equivalent to the problem of recognizing the satisfiable formulas of propositional logic [7]. The fact that hundreds, if not thousands, of NP-complete problems were discovered since then raises an intriguing question. Might any of these equivalent problems admit sufficient structure to allow for efficient search algorithms? Might the beautiful theory of matchings on graphs be useful to find Hamilton cycles? Might the powerful tools of field theory help in solving systems of polynomial equations? In a sense, what the theory of NP-completeness says is that any attempt to give computationally useful structure to the search spaces of such problems is bound to fail. Or at least fail as much as it has failed for the problem of determining truth in the algebra of propositions since its conception by George Boole more than one and a half centuries ago [3]. Proof theory is the branch of mathematical logic that links the syntactic concept of proof with the semantic notion of truth. A formula is unsatisfiable if and only if its negation is a tautology, and tautologies have proofs in any one of the many complete proof systems for propositional logic. Thought this way, the proof theory of propositional logic can be seen as giving structure to the satisfiability problem. Just like an assignment that satisfies a formula is a certificate that a solution exists, a proof of its negation is a certificate that a solution does not exist. The trouble is that while truth assignments are always short, proofs could be exponentially longer. But what if we focus on short proofs? Can reasonably-sized proofs be found in reasonable time? This is the question of automatability of a proof system. In his 1971 article, Cook asked to study “the complexity of theorem proving procedures”, including Resolution, which is the object of our 2019 article, and the rest of this note. A formula in conjunctive normal form, a CNF, is a conjunction of a set of clauses, where a clause is a disjunction of variables or negations of variables. If each clause has at most k