Pseudorandom Generators in Propositional Proof Complexity

Reviewer: Francois Aribaud

This paper studies the complexity of the inconsistent statement for a system of Boolean functions (S): g1(x1,...,xn)=b1,....,gm(x1,...,xn)=bm from the point of view of the combinatorial structure of the supports of the gi. More precisely, a variable xi is inessential for the Boolean function f if f(x1,...,xi-1,0,xi+1,...,xn) = f(x1,...,xi-1,1,xi+1,...,xn), and it is essential in the opposite case. To the system (S), the authors associate the m × n matrix A with entries in 0,1, in which Aij=1 if xj is an essential variable of gi. To go to complexity, one has to encode (S) by a conjunctive normal form (CNF), which is unsatisfiable only if S is inconsistent; the authors describe three such encodings of "reasonable" complexities. The clause is refutable if one can get the empty clause by a chain of resolutions: (a __?__ x), (b __?__ ) maps to (a __?__ b), and one knows some estimates of the size of such a refutation (that is, the number of clauses within it) from the width (the number of literals) of its clauses. Then, the core of the paper (paragraph 3) is the proof of estimates of this width in terms of some technical characteristics of the matrix A, its (r,s,c) expansion coefficients, generalizing the edge expansion properties of ordinary graphs. Then, for suitable matrices A, the proof of inconsistence of all related systems (S) is hard. The paper is a mathematical one that is rigorously written, and thus difficult for the uninformed reader. However, such a reader will appreciate the various and numerous commentaries on the matter, and may learn more on the subject by reading the works in the bibliography. Online Computing Reviews Service