We show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the open problem of whether there are families of k-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width
Total space in resolution / Bonacina, Ilario; Galesi, Nicola; Thapen, Neil. - In: SIAM JOURNAL ON COMPUTING. - ISSN 0097-5397. - ELETTRONICO. - 45:5(2016), pp. 1894-1909. [10.1137/15M1023269]
Total space in resolution
BONACINA, ILARIO;GALESI, NICOLA;
2016
Abstract
We show quadratic lower bounds on the total space used in resolution refutations of random k-CNFs over n variables and of the graph pigeonhole principle and the bit pigeonhole principle for n holes. This answers the open problem of whether there are families of k-CNF formulas of polynomial size that require quadratic total space in resolution. The results follow from a more general theorem showing that, for formulas satisfying certain conditions, in every resolution refutation there is a memory configuration containing many clauses of large width| File | Dimensione | Formato | |
|---|---|---|---|
|
Galesi_Total_2016.pdf
solo utenti autorizzati
Tipologia:
Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza:
Tutti i diritti riservati (All rights reserved)
Dimensione
392.07 kB
Formato
Adobe PDF
|
392.07 kB | Adobe PDF | Contatta l'autore |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
