Strong Size Lower Bounds for (a Subsystem of) Resolution

  • Ilario Bonacina


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