We study the space complexity of refuting unsatisfiable random k-CNFs in the Resolution proof system. We prove that for Delta> 1 and any epsilon > 0, with high probability a random k-CNF over n variables and Delta n clauses requires resolution clause space of Omega(n). For constant this gives us linear, optimal, lower bounds on the clause space.
Space Complexity of Random Formulae in Resolution / BEN SASSON, E.; Galesi, Nicola. - STAMPA. - 16:(2001), pp. 42-51. (Intervento presentato al convegno 16th Annual IEEE Conference on Computational Complexity tenutosi a Chicago Il USA) [10.1109/CCC.2001.933871].
Space Complexity of Random Formulae in Resolution
GALESI, NICOLA
2001
Abstract
We study the space complexity of refuting unsatisfiable random k-CNFs in the Resolution proof system. We prove that for Delta> 1 and any epsilon > 0, with high probability a random k-CNF over n variables and Delta n clauses requires resolution clause space of Omega(n). For constant this gives us linear, optimal, lower bounds on the clause space.File allegati a questo prodotto
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
