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.