Saarland University
Department of Computer Science
Computational Complexity
Computational Complexity




Computational Complexity - Research Seminar

Radu Curticapean: Short proofs for unsatisfiability of dense random 3CNF formulas

April 5, 2011, 10:15 a.m.
E 1 3, Room 415

This talk is mainly based on the paper Recognizing more unsatisfiable random 3-SAT instances efficiently by J. Friedman and A. Goerdt.

It is known that satisfiability of random 3CNF formulas exhibits a threshold behavior: There is a function c(n) in O(1) such that formulas with (1-eps)*c(n)*n clauses are satisfiable with high probability, while formulas with (1+eps)*c(n)*n clauses are unsatisfiable w.h.p.

In this talk, we consider random formulas whose expected number of clauses exceeds the unsatisfiability threshold. We present the results of the aforementioned paper, which state that unsatisfiability of random 3CNF formulas with n^(1.5+eps) expected clauses admits a proof system with poly-length proofs. This proof system satisfies only a relaxed notion of completeness: [...]