Strong Size Lower Bounds for (a Subsystem of) Resolution



In this chapter we put the spotlight again on resolution size and in particular on its connection with conjectures about the exact complexity of the k-SAT problem, that is the conjectures known as the Exponential Time Hypothesis (ETH) and the Strong Exponential Time Hypothesis (SETH). We show a strong width lower bound (Theorem 8.1) and a strong size lower bound for a subsystem of resolution. The lower bounds are stronger than the one we could get immediately from the size-width inequality, eq. (2.10).


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