2020/01/07 by Susanna F. de Rezende, Or Meir, de Rezende, Susanna F. +9 · 1 citation
Computer Science · Decision Sciences · Mathematics · #Auction Theory and Applications #Benford’s Law and Fraud Detection #Complexity and Algorithms in Graphs #Computational Complexity (cs.CC) #Discrete Mathematics (cs.DM) #F.2.2 #F.2.3 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · pdf · doi:10.48550/arxiv.2001.02144
openalex publication_date 2020/01/07 · openalex created_date 2022/07/26 · openalex updated_date 2026/07/28
We significantly strengthen and generalize the theorem lifting\nNullstellensatz degree to monotone span program size by Pitassi and Robere\n(2018) so that it works for any gadget with high enough rank, in particular,\nfor useful gadgets such as equality and greater-than. We apply our generalized\ntheorem to solve two open problems:\n * We present the first result that demonstrates a separation in proof power\nfor cutting planes with unbounded versus polynomially bounded coefficients.\nSpecifically, we exhibit CNF formulas that can be refuted in quadratic length\nand constant line space in cutting planes with unbounded coefficients, but for\nwhich there are no refutations in subexponential length and subpolynomial line\nspace if coefficients are restricted to be of polynomial magnitude.\n * We give the first explicit separation between monotone Boolean formulas and\nmonotone real formulas. Specifically, we give an explicit family of functions\nthat can be computed with monotone real formulas of nearly linear size but\nrequire monotone Boolean formulas of exponential size. Previously only a\nnon-explicit separation was known.\n An important technical ingredient, which may be of independent interest, is\nthat we show that the Nullstellensatz degree of refuting the pebbling formula\nover a DAG G over any field coincides exactly with the reversible pebbling\nprice of G. In particular, this implies that the standard decision tree\ncomplexity and the parity decision tree complexity of the corresponding\nfalsified clause search problem are equal.\n