In this chapter we recall some basic general facts about the proof complexity of resolution [Bla37, Rob65]. This will be a common background for the results in Chap. 3 and Chap. 8. First we describe the most common restrictions placed on the type of resolution refutations, that is regular and tree-like resolution refutations (Sect. 2.1), then we prove a non-trivial size upper bound (Sect. 2.2) and finally we move to the complexity measures known as width and asymmetric width (Sect. 2.3).
Unable to display preview. Download preview PDF.