[Proof Complexity] Survey chapter on proof complexity and SAT solving --- comments welcome!

[Jakob Nordström]

Dear colleagues,

Sam Buss and yours truly have been asked to write a chapter on proof complexity for the 2nd edition of the Handbook of Satisfiability. The idea is to try cover the areas of proof complexity that are most relevant from an applied SAT solving perspective, and to explain the connections between propositional proof systems and satisfiability algorithms. Our hope is that this could be interesting for both theoreticians and practitioners who want to "cross the aisle" and see more of what the other side is about.

This is a truly daunting task, though, and now we would like to ask for your assistance. The survey is nearing completion* (we hope), and the current version can be found at

https://www.math.ucsd.edu/~sbuss/ResearchWeb/ProofComplexitySAT/ProofComplexityChapter.pdf
http://www.csc.kth.se/~jakobn/research/ProofComplexityChapter.pdf

We would be most grateful for all kinds of feedback on the current manuscript. There are sure to be lots of typos, probably quite a few unclear passages, and maybe even some glaring errors. We might also have omitted recent news (or old news) that we are not aware of. Any help that you, dear colleagues, could provide to address such shortcomings will be gratefully acknowledged.

The only constraint we have is that the manuscript cannot grow to be much longer --- in fact, we are already wildly over the page limit. Thus, some of the missing material that you will detect might actually be conscious choices from our side, but we are still interested in hearing about any omissions you find to be particularly outrageous.

Best regards,
Jakob (and Sam)

(*) The current status of the manuscript is that it is finished (i.e., in beta version) up to page 63. Sections 1.8.2-1.8.3 (pages 63-66) are incomplete. Pages 66-73 should again be in beta, but then the concluding remarks in Sec 1.13 remain to be written.