Počet záznamů: 1
Lifting with simple gadgets and applications to circuit and proof complexity
- 1.
SYSNO ASEP 0539558 Druh ASEP C - Konferenční příspěvek (mezinárodní konf.) Zařazení RIV D - Článek ve sborníku Název Lifting with simple gadgets and applications to circuit and proof complexity Tvůrce(i) de Rezende, Susanna F. (MU-W) ORCID, SAI, RID
Meir, O. (IL)
Norström, J. (SE)
Pitassi, T. (US)
Robere, R. (CA)
Vinyals, M. (IL)Zdroj.dok. 2020 IEEE 61st Annual Symposium on Foundations of Computer Science. - Los Alamitos : IEEE, 2020 - ISBN 978-1-7281-9622-0 Rozsah stran s. 24-30 Poč.str. 7 s. Forma vydání Tištěná - P Akce 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020 Datum konání 16.11.2020 - 19.11.2020 Místo konání Durham Země US - Spojené státy americké Typ akce WRD Jazyk dok. eng - angličtina Země vyd. US - Spojené státy americké Klíč. slova circuit complexity ; communication complexity ; cutting planes Vědní obor RIV IN - Informatika Obor OECD Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8) Institucionální podpora MU-W - RVO:67985840 UT WOS 000652333400003 EID SCOPUS 85100337762 DOI 10.1109/FOCS46700.2020.00011 Anotace We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve three open problems: •We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. •We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. •We give the strongest separation to-date between monotone Boolean formulas and monotone Boolean circuits. Namely, we show that the classical GEN problem, which has polynomial-size monotone Boolean circuits, requires monotone Boolean formulas of size 2{Omega(n text{polylog}(n))}. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal. This is an extended abstract. The full version of the paper is available at https://arxiv.org/abs/2001.02144. Pracoviště Matematický ústav Kontakt Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Rok sběru 2021
Počet záznamů: 1