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.

Unable to display preview. Download preview PDF.

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Departament de Ciències de la ComputacióUniversitat Politècnica de CatalunyaBarcelonaSpain

Personalised recommendations