期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2001
卷号：2001
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：We study the space complexity of refuting unsatisfiable random k -CNFs in the Resolution proof system. We prove that for any large enough , with high probability a random k -CNF over n variables and n clauses requires resolution clause space of ( n − 1+ k − 2 − ) , for any 0 1 2 . For constant , this gives us linear, optimal, lower bounds on the clause space. A nice consequence of this lower bound is the first lower bound for size of treelike resolution refutations of random 3 -CNFs with clause density > \sqrt{n}"> n . This bound is nearly tight. Specifically, we show that with high probability, a random 3 -CNF with n clauses requires treelike refutation size of exp ( ( n 1 − 1+ )) , for any 0 1 2 . Our space lower bound is the consequence of three main contributions. 1. We introduce a 2-player Matching Game on bipartite graphs G to prove that there are no perfect matchings in G . 2. We reduce lower bounds for the clause space of a formula F in Resolution to lower bounds for the complexity of the game played on the bipartite graph G ( F ) associated with F . 3. We prove that the complexity of the game is large whenever G is an expander graph. Finally, a simple probabilistic analysis shows that for a random formula F , with high probability G ( F ) is an expander. We also extend our result to the case of G − P H P , a generalization of the pigeonhole Principle based on bipartite graphs G . We prove that the clause space for G − P H P can be reduced to the game complexity on G .
关键词：Proof Complexity , Random CNF , Resolution , satisfiability , Space
, with high probability a random k -CNF over n variables and 
