Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Pseudorandom generators in propositional proof complexity
Alekhnovich M., Ben-Sasson E., Razborov A., Wigderson A. SIAM Journal on Computing34 (1):67-88,2005.Type:Article
Date Reviewed: Aug 4 2005

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.

Reviewer:  F. Aribaud Review #: CR131628 (0602-0183)
Bookmark and Share
 
Proof Theory (F.4.1 ... )
 
 
Mathematical Logic (F.4.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Proof Theory": Date
On the strength of temporal proofs
Andréka H., Németi I., Sain I. Theoretical Computer Science 80(2): 125-151, 1991. Type: Article
Apr 1 1992
Completion for unification
Doggaz N., Kirchner C. (ed) Theoretical Computer Science 85(2): 231-251, 1991. Type: Article
Aug 1 1992
Proof normalization with nonstandard objects
Goto S. Theoretical Computer Science 85(2): 333-351, 1991. Type: Article
Aug 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy