Document

**Published in:** LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.

Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vinyals_et_al:LIPIcs.SAT.2023.27, author = {Vinyals, Marc and Li, Chunxiao and Fleming, Noah and Kolokolova, Antonina and Ganesh, Vijay}, title = {{Limits of CDCL Learning via Merge Resolution}}, booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)}, pages = {27:1--27:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-286-0}, ISSN = {1868-8969}, year = {2023}, volume = {271}, editor = {Mahajan, Meena and Slivovsky, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.27}, URN = {urn:nbn:de:0030-drops-184894}, doi = {10.4230/LIPIcs.SAT.2023.27}, annote = {Keywords: proof complexity, resolution, merge resolution, CDCL, learning scheme} }

Document

Track A: Algorithms, Complexity and Games

**Published in:** LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Lifting arguments show that the complexity of a function in one model is essentially that of a related function (often the composition of the original function with a small function called a gadget) in a more powerful model. Lifting has been used to prove strong lower bounds in communication complexity, proof complexity, circuit complexity and many other areas.
We present a lifting construction for constant depth unbounded fan-in circuits. Given a function f, we construct a function g, so that the depth d+1 circuit complexity of g, with a certain restriction on bottom fan-in, is controlled by the depth d circuit complexity of f, with the same restriction. The function g is defined as f composed with a parity function. With some quantitative losses, average-case and general depth-d circuit complexity can be reduced to circuit complexity with this bottom fan-in restriction. As a consequence, an algorithm to approximate the depth d (for any d > 3) circuit complexity of given (truth tables of) Boolean functions yields an algorithm for approximating the depth 3 circuit complexity of functions, i.e., there are quasi-polynomial time mapping reductions between various gap-versions of AC⁰-MCSP. Our lifting results rely on a blockwise switching lemma that may be of independent interest.
We also show some barriers on improving the efficiency of our reductions: such improvements would yield either surprisingly efficient algorithms for MCSP or stronger than known AC⁰ circuit lower bounds.

Marco Carmosino, Kenneth Hoover, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. Lifting for Constant-Depth Circuits and Applications to MCSP. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 44:1-44:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{carmosino_et_al:LIPIcs.ICALP.2021.44, author = {Carmosino, Marco and Hoover, Kenneth and Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina}, title = {{Lifting for Constant-Depth Circuits and Applications to MCSP}}, booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)}, pages = {44:1--44:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-195-5}, ISSN = {1868-8969}, year = {2021}, volume = {198}, editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.44}, URN = {urn:nbn:de:0030-drops-141135}, doi = {10.4230/LIPIcs.ICALP.2021.44}, annote = {Keywords: circuit complexity, constant-depth circuits, lifting theorems, Minimum Circuit Size Problem, reductions, Switching Lemma} }

Document

Track A: Algorithms, Complexity and Games

**Published in:** LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Minimum Circuit Size Problem (MCSP) asks to decide if a given truth table of an n-variate boolean function has circuit complexity less than a given parameter s. We prove that MCSP is hard for constant-depth circuits with mod p gates, for any prime p >= 2 (the circuit class AC^0[p]). Namely, we show that MCSP requires d-depth AC^0[p] circuits of size at least exp(N^{0.49/d}), where N=2^n is the size of an input truth table of an n-variate boolean function. Our circuit lower bound proof shows that MCSP can solve the coin problem: distinguish uniformly random N-bit strings from those generated using independent samples from a biased random coin which is 1 with probability 1/2+N^{-0.49}, and 0 otherwise. Solving the coin problem with such parameters is known to require exponentially large AC^0[p] circuits. Moreover, this also implies that MAJORITY is computable by a non-uniform AC^0 circuit of polynomial size that also has MCSP-oracle gates. The latter has a few other consequences for the complexity of MCSP, e.g., we get that any boolean function in NC^1 (i.e., computable by a polynomial-size formula) can also be computed by a non-uniform polynomial-size AC^0 circuit with MCSP-oracle gates.

Alexander Golovnev, Rahul Ilango, Russell Impagliazzo, Valentine Kabanets, Antonina Kolokolova, and Avishay Tal. AC^0[p] Lower Bounds Against MCSP via the Coin Problem. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 66:1-66:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{golovnev_et_al:LIPIcs.ICALP.2019.66, author = {Golovnev, Alexander and Ilango, Rahul and Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina and Tal, Avishay}, title = {{AC^0\lbrackp\rbrack Lower Bounds Against MCSP via the Coin Problem}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {66:1--66:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.66}, URN = {urn:nbn:de:0030-drops-106422}, doi = {10.4230/LIPIcs.ICALP.2019.66}, annote = {Keywords: Minimum Circuit Size Problem (MCSP), circuit lower bounds, AC0\lbrackp\rbrack, coin problem, hybrid argument, MKTP, biased random boolean functions} }

Document

**Published in:** LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)

We introduce and develop a new semi-algebraic proof system, called Stabbing Planes that is in the style of DPLL-based modern SAT solvers. As with DPLL, there is only one rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane a x >= b with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying a x >= b, the points satisfying a x <= b-1, and the middle slab b-1 < a x < b. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show somewhat surprisingly that Stabbing Planes can efficiently simulate Cutting Planes, and moreover, is strictly stronger than Cutting Planes under a reasonable conjecture. We prove linear lower bounds on the rank of Stabbing Planes refutations, by adapting
a lifting argument in communication complexity.

Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing Planes. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{beame_et_al:LIPIcs.ITCS.2018.10, author = {Beame, Paul and Fleming, Noah and Impagliazzo, Russell and Kolokolova, Antonina and Pankratov, Denis and Pitassi, Toniann and Robere, Robert}, title = {{Stabbing Planes}}, booktitle = {9th Innovations in Theoretical Computer Science Conference (ITCS 2018)}, pages = {10:1--10:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-060-6}, ISSN = {1868-8969}, year = {2018}, volume = {94}, editor = {Karlin, Anna R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.10}, URN = {urn:nbn:de:0030-drops-83418}, doi = {10.4230/LIPIcs.ITCS.2018.10}, annote = {Keywords: Complexity Theory, Proof Complexity, Communication Complexity, Cutting Planes, Semi-Algebraic Proof Systems, Pseudo Boolean Solvers, SAT solvers, Inte} }

Document

**Published in:** LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

The Black-Box Hypothesisstates that any property of Boolean functions decided efficiently (e.g., in BPP) with inputs represented by circuits can also be decided efficiently in the black-box setting, where an algorithm is given an oracle access to the input function and an upper bound on its circuit size. If this hypothesis is true, then P neq NP. We focus on the consequences of the hypothesis being false, showing that (under general conditions on the structure of a counterexample) it implies a non-trivial algorithm for CSAT. More specifically, we show that if there is a property F of boolean functions such that F has high sensitivity on some input function f of subexponential circuit complexity (which is a sufficient condition for F being a counterexample to the Black-Box Hypothesis), then CSAT is solvable by a subexponential-size circuit family. Moreover, if such a counterexample F is symmetric, then CSAT is in Ppoly. These results provide some evidence towards the conjecture (made in this paper) that the Black-Box Hypothesis is false if and only if CSAT is easy.

Russell Impagliazzo, Valentine Kabanets, Antonina Kolokolova, Pierre McKenzie, and Shadab Romani. Does Looking Inside a Circuit Help?. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 1:1-1:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{impagliazzo_et_al:LIPIcs.MFCS.2017.1, author = {Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina and McKenzie, Pierre and Romani, Shadab}, title = {{Does Looking Inside a Circuit Help?}}, booktitle = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)}, pages = {1:1--1:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-046-0}, ISSN = {1868-8969}, year = {2017}, volume = {83}, editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.1}, URN = {urn:nbn:de:0030-drops-80975}, doi = {10.4230/LIPIcs.MFCS.2017.1}, annote = {Keywords: Black-Box Hypothesis, Rice's theorem, circuit complexity, SAT, sensitivity of boolean functions, decision tree complexity} }

Document

**Published in:** LIPIcs, Volume 67, 8th Innovations in Theoretical Computer Science Conference (ITCS 2017)

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson (2002), and show that this analysis can be formalized in the bounded arithmetic system VNC^1 (corresponding to the "NC^1 reasoning"). As a corollary, we prove the assumption made by Jerabek (2011) that a construction of certain bipartite expander graphs can be formalized in VNC^1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlak (2002).

Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucky. Expander Construction in VNC1. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 31:1-31:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{buss_et_al:LIPIcs.ITCS.2017.31, author = {Buss, Sam and Kabanets, Valentine and Kolokolova, Antonina and Koucky, Michal}, title = {{Expander Construction in VNC1}}, booktitle = {8th Innovations in Theoretical Computer Science Conference (ITCS 2017)}, pages = {31:1--31:26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-029-3}, ISSN = {1868-8969}, year = {2017}, volume = {67}, editor = {Papadimitriou, Christos H.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2017.31}, URN = {urn:nbn:de:0030-drops-81871}, doi = {10.4230/LIPIcs.ITCS.2017.31}, annote = {Keywords: expander graphs, bounded arithmetic, alternating log time, sequent calculus, monotone propositional logic} }

Document

**Published in:** LIPIcs, Volume 81, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017)

We generalize the "learning algorithms from natural properties" framework of [CIKK16] to get agnostic learning algorithms from natural properties with extra features. We show that if a natural property (in the sense of Razborov and Rudich [RR97]) is useful also against functions that are close to the class of "easy" functions, rather than just against "easy" functions, then it can be used to get an agnostic learning algorithm over the uniform distribution with membership queries.
* For AC0[q], any prime q (constant-depth circuits of polynomial size, with AND, OR, NOT, and MODq gates of unbounded fanin), which happens to have a natural property with the requisite extra feature by [Raz87, Smo87, RR97], we obtain the first agnostic learning algorithm for AC0[q], for every prime q. Our algorithm runs in randomized quasi-polynomial time, uses membership queries, and outputs a circuit for a given Boolean function f that agrees with f on all but at most polylog(n)*opt fraction of inputs, where opt is the relative distance between f and the closest function h in the class AC0[q].
* For the ideal case, a natural proof of strongly exponential correlation circuit lower bounds against a circuit class C containing AC0[2] (i.e., circuits of size exp(Omega(n)) cannot compute some n-variate function even with exp(-Omega(n)) advantage over random guessing) would yield a polynomial-time query agnostic learning algorithm for C with the approximation error O(opt).

Marco L. Carmosino, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. Agnostic Learning from Tolerant Natural Proofs. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 81, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{carmosino_et_al:LIPIcs.APPROX-RANDOM.2017.35, author = {Carmosino, Marco L. and Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina}, title = {{Agnostic Learning from Tolerant Natural Proofs}}, booktitle = {Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017)}, pages = {35:1--35:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-044-6}, ISSN = {1868-8969}, year = {2017}, volume = {81}, editor = {Jansen, Klaus and Rolim, Jos\'{e} D. P. and Williamson, David P. and Vempala, Santosh S.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2017.35}, URN = {urn:nbn:de:0030-drops-75842}, doi = {10.4230/LIPIcs.APPROX-RANDOM.2017.35}, annote = {Keywords: agnostic learning, natural proofs, circuit lower bounds, meta-algorithms, AC0\lbrackq\rbrack, Nisan-Wigderson generator} }

Document

**Published in:** LIPIcs, Volume 50, 31st Conference on Computational Complexity (CCC 2016)

Based on Hastad's (1986) circuit lower bounds, Linial, Mansour, and Nisan (1993) gave a quasipolytime learning algorithm for AC^0 (constant-depth circuits with AND, OR, and NOT gates), in the PAC model over the uniform distribution. It was an open question to get a learning algorithm (of any kind) for the class of AC^0[p] circuits (constant-depth, with AND, OR, NOT, and MOD_p gates for a prime p).
Our main result is a quasipolytime learning algorithm for AC^0[p] in the PAC model over the uniform distribution with membership queries. This algorithm is an application of a general connection we show to hold between natural proofs (in the sense of Razborov and Rudich (1997)) and learning algorithms. We argue that a natural proof of a circuit lower bound against any (sufficiently powerful) circuit class yields a learning algorithm for the same circuit class. As the lower bounds against AC^0[p] by Razborov (1987) and Smolensky (1987) are natural, we obtain our learning algorithm for AC^0[p].

Marco L. Carmosino, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. Learning Algorithms from Natural Proofs. In 31st Conference on Computational Complexity (CCC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 50, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{carmosino_et_al:LIPIcs.CCC.2016.10, author = {Carmosino, Marco L. and Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina}, title = {{Learning Algorithms from Natural Proofs}}, booktitle = {31st Conference on Computational Complexity (CCC 2016)}, pages = {10:1--10:24}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-008-8}, ISSN = {1868-8969}, year = {2016}, volume = {50}, editor = {Raz, Ran}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2016.10}, URN = {urn:nbn:de:0030-drops-58557}, doi = {10.4230/LIPIcs.CCC.2016.10}, annote = {Keywords: natural proofs, circuit complexity, lower bounds, learning, compression} }

Document

**Published in:** LIPIcs, Volume 40, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2015)

We tighten the connections between circuit lower bounds and derandomization for each of the following three types of derandomization:
- general derandomization of promiseBPP (connected to Boolean circuits),
- derandomization of Polynomial Identity Testing (PIT) over fixed finite fields (connected to arithmetic circuit lower bounds over the same field), and
- derandomization of PIT over the integers (connected to arithmetic circuit lower bounds over the integers).
We show how to make these connections uniform equivalences, although at the expense of using somewhat less common versions of complexity classes and for a less studied notion of inclusion.
Our main results are as follows:
1. We give the first proof that a non-trivial (nondeterministic subexponential-time) algorithm for PIT over a fixed finite field yields arithmetic circuit lower bounds.
2. We get a similar result for the case of PIT over the integers, strengthening a result of Jansen and Santhanam [JS12] (by removing the need for advice).
3. We derive a Boolean circuit lower bound for NEXP intersect coNEXP from the assumption of sufficiently strong non-deterministic derandomization of promiseBPP (without advice), as well as from the assumed existence of an NP-computable non-empty property of Boolean functions useful for proving superpolynomial circuit lower bounds (in the sense of natural proofs of [RR97]); this strengthens the related results of [IKW02].
4. Finally, we turn all of these implications into equivalences for appropriately defined promise classes and for a notion of robust inclusion/separation (inspired by [FS11]) that lies between the classical "almost everywhere" and "infinitely often" notions.

Marco L. Carmosino, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. Tighter Connections between Derandomization and Circuit Lower Bounds. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 40, pp. 645-658, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{carmosino_et_al:LIPIcs.APPROX-RANDOM.2015.645, author = {Carmosino, Marco L. and Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina}, title = {{Tighter Connections between Derandomization and Circuit Lower Bounds}}, booktitle = {Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2015)}, pages = {645--658}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-89-7}, ISSN = {1868-8969}, year = {2015}, volume = {40}, editor = {Garg, Naveen and Jansen, Klaus and Rao, Anup and Rolim, Jos\'{e} D. P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2015.645}, URN = {urn:nbn:de:0030-drops-53285}, doi = {10.4230/LIPIcs.APPROX-RANDOM.2015.645}, annote = {Keywords: derandomization, circuit lower bounds, polynomial identity testing, promise BPP, hardness vs. randomness} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 9421, Algebraic Methods in Computational Complexity (2010)

Non-relativization of complexity issues can be interpreted
as giving some evidence that these issues cannot be resolved
by "black-box" techniques. In the early 1990's, a sequence of
important non-relativizing results was proved, mainly using
algebraic techniques. Two approaches have been proposed
to understand the power and limitations of these algebraic
techniques: (1) Fortnow gives a construction of a class
of oracles which have a similar algebraic and logical structure,
although they are arbitrarily powerful. He shows that
many of the non-relativizing results proved using algebraic
techniques hold for all such oracles, but he does not show,
e.g., that the outcome of the "P vs. NP" question differs
between different oracles in that class. (2) Aaronson and
Wigderson give definitions of algebrizing separations and
collapses of complexity classes, by comparing classes relative
to one oracle to classes relative to an algebraic extension of
that oracle. Using these definitions, they show both that
the standard collapses and separations "algebrize" and that
many of the open questions in complexity fail to "algebrize",
suggesting that the arithmetization technique is close to its
limits. However, it is unclear how to formalize algebrization
of more complicated complexity statements than collapses
or separations, and whether the algebrizing statements are,
e.g., closed under modus ponens; so it is conceivable that
several algebrizing premises could imply (in a relativizing
way) a non-algebrizing conclusion.
Here, building on the work of Arora, Impagliazzo,
and Vazirani [4], we propose an axiomatic approach to "algebrization",
which complements and clarifies the approaches
of Fortnow and Aaronso&Wigderson. We present logical theories formalizing the notion of algebrizing techniques so that most algebrizing results
are provable within our theories and separations requiring
non-algebrizing techniques are independent of them.
Our theories extend the [AIV] theory formalizing relativization
by adding an Arithmetic Checkability axiom.
We show the following: (i) Arithmetic checkability holds
relative to arbitrarily powerful oracles (since Fortnow's algebraic oracles all satisfy Arithmetic Checkability
axiom); by contrast, Local Checkability of [AIV] restricts the
oracle power to NP cap co-NP. (ii) Most of the algebrizing
collapses and separations from [AW], such as IP = PSPACE,
NP subset ZKIP if one-way functions exist, MA-EXP not in P/poly,
etc., are provable from Arithmetic Checkability. (iii) Many
of the open complexity questions (shown to require nonalgebrizing
techniques in [AW]), such as "P vs. NP", "NP vs.
BPP", etc., cannot be proved from Arithmetic Checkability.
(iv) Arithmetic Checkability is also insufficient to prove one
known result, NEXP = MIP.

Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. An Axiomatic Approach to Algebrization. In Algebraic Methods in Computational Complexity. Dagstuhl Seminar Proceedings, Volume 9421, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{impagliazzo_et_al:DagSemProc.09421.3, author = {Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina}, title = {{An Axiomatic Approach to Algebrization}}, booktitle = {Algebraic Methods in Computational Complexity}, pages = {1--19}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {9421}, editor = {Manindra Agrawal and Lance Fortnow and Thomas Thierauf and Christopher Umans}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09421.3}, URN = {urn:nbn:de:0030-drops-24150}, doi = {10.4230/DagSemProc.09421.3}, annote = {Keywords: Oracles, arithmetization, algebrization} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail