We analyze size and space complexity of Res(k), a family of proof systems introduced by Kraj ́ıˇcek in [16] which extend Resolu- tion by allowing disjunctions of conjunctions of up to k ≥ 1 literals. We prove the following results: (1) The treelike Res(k) proof systems form a strict hierarchy with respect to proof size and also with respect to space. (2) Resolution polynomially simulates treelike Res(k), and is almost ex- ponentially separated from treelike Res(k). (3) The space lower bounds known for Resolution also carry over to Res(k). We obtain almost opti- mal space lower bounds for PHPn, GTn, Random Formulas, CTn, and Tseitin Tautologies.
On the complexity of resolution with bounded conjunctions / Juan Luis, Esteban; Galesi, Nicola; Jochen, Messner. - STAMPA. - 2380:(2002), pp. 220-231. (Intervento presentato al convegno Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, tenutosi a Malaga, Spain,) [10.1007/3-540-45465-9_20].
On the complexity of resolution with bounded conjunctions.
GALESI, NICOLA
;
2002
Abstract
We analyze size and space complexity of Res(k), a family of proof systems introduced by Kraj ́ıˇcek in [16] which extend Resolu- tion by allowing disjunctions of conjunctions of up to k ≥ 1 literals. We prove the following results: (1) The treelike Res(k) proof systems form a strict hierarchy with respect to proof size and also with respect to space. (2) Resolution polynomially simulates treelike Res(k), and is almost ex- ponentially separated from treelike Res(k). (3) The space lower bounds known for Resolution also carry over to Res(k). We obtain almost opti- mal space lower bounds for PHPn, GTn, Random Formulas, CTn, and Tseitin Tautologies.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
