More on the relative strength of counting principles
Paul W. Beame, Søren Kamaric Riis · DIMACS series in discrete mathematics and theoretical computer science · 1997
this paper we attempt to give as complete a presentation as possible. We now outline the structure of the argument, giving references for the key techniques. We use the notion of a k-evaluation due to Kraj'icek, Pudl'ak, and Woods [13], incorporating 2 the matching decision trees of Pitassi, Beame, Impagliazzo [15], and built for any small Frege proof using a switching lemma proved with the methods of Beame [4]. Then, as in the argument of Riis [16] and Beame and Pitassi [8], we show that having a k-evaluation implies the existence of a certain forest of matching decision trees. Following this we show, using a reduction analogous to that of Beame, Impagliazzo, Kraj'icek, Pitassi, and Pudl'ak [6], that the existence of such a forest implies a small degree Nullstellensatz refutation of an associated family of polynomials. Finally, the proof that such a small degree refutation does not exist is analogous to that of Buss, Impagliazzo, Kraj'icek, Pudl'ak, Razborov, and Sgall [10]. This last is the main new technical contribution and the reader who is familiar with the other aspects of this paper may wish to skip directly to section 8. In section 9 we combine the arguments from the previous sections to show our main results. 2 Frege Proofs and Counting Principles