Title: Theory / Unimportant / CS / Fundamental / Complexity / Complexity Arora Barak/{ / Proof complexity
Tags: fromMath mathToDef

Name: A resolution
Definition: The process of choosing a variable \(x_i\), two clauses \(x_i\lor C\) and \(\neg x_i\lor C'\) and creating the clause \(C\lor C'\).
Page: 309
Chapter: 15
Section: 2
Variables: \(\{x_1,\dots,x_n\}\) a set of variables,
\(C_1,\dots,C_m\) a set of clauses

Name: Resolution refutation
Definition: A sequence of resolution leading to the empty clause.
Page: 309
Chapter: 15
Section: 2
Variables: \(\{x_1,\dots,x_n\}\) a set of variables, \(C_1,\dots,C_m\) a set of clauses

Question: The resolution refutation of the pigeon hole principle with \(n\) pigeon has size
Answer: at least \(2^{n/20}\).
Page: 310
Chapter: 15
Section: 2
Variables: \(n\in\mathbb N\)
Index: 1
Kind: Theo