Document Open Access Logo

Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework

Authors Alexander Golovnev, Alexander S. Kulikov, Alexander V. Smal, Suguru Tamaki

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.45.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Alexander Golovnev
Alexander S. Kulikov
Alexander V. Smal
Suguru Tamaki

Cite AsGet BibTex

Alexander Golovnev, Alexander S. Kulikov, Alexander V. Smal, and Suguru Tamaki. Circuit Size Lower Bounds and #SAT Upper Bounds Through a General Framework. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 45:1-45:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.MFCS.2016.45

Abstract

Most of the known lower bounds for binary Boolean circuits with unrestricted depth are proved by the gate elimination method. The most efficient known algorithms for the #SAT problem on binary Boolean circuits use similar case analyses to the ones in gate elimination. Chen and Kabanets recently showed that the known case analyses can also be used to prove average case circuit lower bounds, that is, lower bounds on the size of approximations of an explicit function. In this paper, we provide a general framework for proving worst/average case lower bounds for circuits and upper bounds for #SAT that is built on ideas of Chen and Kabanets. A proof in such a framework goes as follows. One starts by fixing three parameters: a class of circuits, a circuit complexity measure, and a set of allowed substitutions. The main ingredient of a proof goes as follows: by going through a number of cases, one shows that for any circuit from the given class, one can find an allowed substitution such that the given measure of the circuit reduces by a sufficient amount. This case analysis immediately implies an upper bound for #SAT. To~obtain worst/average case circuit complexity lower bounds one needs to present an explicit construction of a function that is a disperser/extractor for the class of sources defined by the set of substitutions under consideration. We show that many known proofs (of circuit size lower bounds and upper bounds for #SAT) fall into this framework. Using this framework, we prove the following new bounds: average case lower bounds of 3.24n and 2.59n for circuits over U_2 and B_2, respectively (though the lower bound for the basis B_2 is given for a quadratic disperser whose explicit construction is not currently known), and faster than 2^n #SAT-algorithms for circuits over U_2 and B_2 of size at most 3.24n and 2.99n, respectively. Here by B_2 we mean the set of all bivariate Boolean functions, and by U_2 the set of all bivariate Boolean functions except for parity and its complement.
Keywords
  • circuit complexity
  • lower bounds
  • exponential time algorithms
  • satisfiability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Kazuyuki Amano and Atsushi Saito. A nonuniform circuit class with multilayer of threshold gates having super quasi polynomial size lower bounds against NEXP. In Proceedings of the 9th International Conference on Language and Automata Theory and Applications (LATA), pages 461-472, 2015. Google Scholar
  2. Kazuyuki Amano and Atsushi Saito. A satisfiability algorithm for some class of dense depth two threshold circuits. IEICE Transactions, 98-D(1):108-118, 2015. Google Scholar
  3. Kazuyuki Amano and Jun Tarui. A well-mixed function with circuit complexity 5n: Tightness of the Lachish-Raz-type bounds. Theor. Comput. Sci., 412(18):1646-1651, 2011. Google Scholar
  4. Paul Beame, Russell Impagliazzo, and Srikanth Srinivasan. Approximating AC⁰ by small height decision trees and a deterministic algorithm for #AC⁰ SAT. In Proceedings of the 27th Conference on Computational Complexity (CCC), pages 117-125, 2012. Google Scholar
  5. Eli Ben-Sasson and Ariel Gabizon. Extractors for polynomial sources over fields of constant order and small characteristic. Theory of Computing, 9:665-683, 2013. Google Scholar
  6. Eli Ben-Sasson and Swastik Kopparty. Affine dispersers from subspace polynomials. SIAM J. Comput., 41(4):880-914, 2012. Google Scholar
  7. Eli Ben-Sasson and Emanuele Viola. Short PCPs with projection queries. In Proceedings of the 41st International Colloquium on Automata, Languages, and Programming (ICALP), Part I, pages 163-173, 2014. Google Scholar
  8. Norbert Blum. A Boolean function requiring 3n network size. Theor. Comput. Sci., 28:337-345, 1984. Google Scholar
  9. Harry Buhrman, Lance Fortnow, and Thomas Thierauf. Nonrelativizing separations. In Proceedings of the 13th Annual IEEE Conference on Computational Complexity (CCC), pages 8-12, 1998. Google Scholar
  10. Venkatesan T. Chakaravarthy and Sambuddha Roy. Oblivious symmetric alternation. In Proceedings of the 23rd Annual Symposium on Theoretical Aspects of Computer Science (STACS), pages 230-241, 2006. Google Scholar
  11. Venkatesan T. Chakaravarthy and Sambuddha Roy. Arthur and Merlin as oracles. Computational Complexity, 20(3):505-558, 2011. Google Scholar
  12. Ruiwen Chen. Satisfiability algorithms and lower bounds for Boolean formulas over finite bases. In Proceedings of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS), Part II, pages 223-234, 2015. Google Scholar
  13. Ruiwen Chen and Valentine Kabanets. Correlation bounds and #SAT algorithms for small linear-size circuits. In Proceedings of the 21st International Conference on Computing and Combinatorics (COCOON), pages 211-222, 2015. Google Scholar
  14. Ruiwen Chen, Valentine Kabanets, Antonina Kolokolova, Ronen Shaltiel, and David Zuckerman. Mining circuit lower bound proofs for meta-algorithms. Computational Complexity, 24(2):333-392, 2015. Google Scholar
  15. Ruiwen Chen, Valentine Kabanets, and Nitin Saurabh. An improved deterministic #SAT algorithm for small De Morgan formulas. In Proceedings of the 39th International Symposium on Mathematical Foundations of Computer Science (MFCS), Part II, pages 165-176, 2014. Google Scholar
  16. Ruiwen Chen and Rahul Santhanam. Improved algorithms for sparse MAX-SAT and MAX-k-CSP. In Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 33-45, 2015. Google Scholar
  17. Ruiwen Chen, Rahul Santhanam, and Srikanth Srinivasan. Average-case lower bounds and satisfiability algorithms for small threshold circuits. In Proceedings of the 31th Conference on Computational Complexity (CCC), pages 1:1-1:35, 2016. Google Scholar
  18. Benny Chor, Oded Goldreich, Johan Håstad, Joel Friedman, Steven Rudich, and Roman Smolensky. The bit extraction problem of t-resilient functions (preliminary version). In Proceedings of the 26th Annual Symposium on Foundations of Computer Science (FOCS), pages 396-407, 1985. Google Scholar
  19. Gil Cohen and Igor Shinkar. The complexity of DNF of parities. In Proceedings of the 7th Innovations in Theoretical Computer Science (ITCS) Conference, pages 47-58, 2016. Google Scholar
  20. Evgeny Demenkov and Alexander S. Kulikov. An elementary proof of a 3n - o(n) lower bound on the circuit complexity of affine dispersers. In Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 256-265, 2011. Google Scholar
  21. Evgeny Demenkov, Alexander S. Kulikov, Olga Melanich, and Ivan Mihajlin. New lower bounds on circuit size of multi-output functions. Theory of Computing Systems, 56(4):630-642, 2015. Google Scholar
  22. Yevgeniy Dodis. Exposure-resilient cryptography. PhD thesis, Massachusetts Institute of Technology, 2000. Google Scholar
  23. Zeev Dvir. Extractors for varieties. Computational Complexity, 21(4):515-572, 2012. Google Scholar
  24. Zeev Dvir, Ariel Gabizon, and Avi Wigderson. Extractors and rank extractors for polynomial sources. Computational Complexity, 18(1):1-58, 2009. Google Scholar
  25. Magnus Gausdal Find, Alexander Golovnev, Edward Hirsch, and Alexander Kulikov. A better-than-3n lower bound for the circuit complexity of an explicit function. Electronic Colloquium on Computational Complexity (ECCC), TR15-166, 2015. Google Scholar
  26. Alexander Golovnev and Alexander S. Kulikov. Weighted gate elimination: Boolean dispersers for quadratic varieties imply improved circuit lower bounds. In Proceedings of the 7th Innovations in Theoretical Computer Science (ITCS) Conference, pages 405-411, 2016. Google Scholar
  27. Alexander Golovnev, Alexander S. Kulikov, Alexander Smal, and Suguru Tamaki. Circuit size lower bounds and #sat upper bounds through a general framework. Electronic Colloquium on Computational Complexity (ECCC), TR16-022, 2016. Google Scholar
  28. Johan Håstad. On the correlation of parity and small-depth circuits. SIAM J. Comput., 43(5):1699-1708, 2014. Google Scholar
  29. Russell Impagliazzo, William Matthews, and Ramamohan Paturi. A satisfiability algorithm for AC⁰. In Proceedings of the 23rd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 961-972, 2012. Google Scholar
  30. Russell Impagliazzo, Ramamohan Paturi, and Stefan Schneider. A satisfiability algorithm for sparse depth two threshold circuits. In Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 479-488, 2013. Google Scholar
  31. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512-530, 2001. Google Scholar
  32. Kazuo Iwama and Hiroki Morizumi. An explicit lower bound of 5n - o(n) for Boolean circuits. In Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 353-364, 2002. Google Scholar
  33. Hamid Jahanjou, Eric Miles, and Emanuele Viola. Local reductions. In Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP), Part I, pages 749-760, 2015. Google Scholar
  34. Arist Kojevnikov and Alexander S. Kulikov. Circuit complexity and multiplicative complexity of Boolean functions. In Proceedings of the 6th Conference on Computability in Europe (CiE), pages 239-245, 2010. Google Scholar
  35. Ilan Komargodski and Ran Raz. Average-case lower bounds for formula size. In Proceedings of the 45th Symposium on Theory of Computing (STOC), pages 171-180, 2013. Google Scholar
  36. Ilan Komargodski, Ran Raz, and Avishay Tal. Improved average-case lower bounds for De Morgan formula size. In Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 588-597, 2013. Google Scholar
  37. Oliver Kullmann. Fundaments of branching heuristics. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 205-244. IOS Press, 2009. Google Scholar
  38. Oded Lachish and Ran Raz. Explicit lower bound of 4.5n - o(n) for Boolean circuits. In Proceedings on 33rd Annual ACM Symposium on Theory of Computing (STOC), pages 399-408, 2001. Google Scholar
  39. Xin Li. A new approach to affine extractors and dispersers. In Proceedings of the 26th Annual IEEE Conference on Computational Complexity (CCC), pages 137-147, 2011. Google Scholar
  40. Xin Li. Improved two-source extractors, and affine extractors for polylogarithmic entropy. Electronic Colloquium on Computational Complexity (ECCC), TR15-125, 2015. Google Scholar
  41. Daniel Lokshtanov, Dániel Marx, and Saket Saurabh. Lower bounds based on the exponential time hypothesis. Bulletin of the EATCS, 105:41-72, 2011. Google Scholar
  42. Dániel Marx. Consequences of ETH: Tight bounds for various problems. In Fine-Grained Complexity and Algorithm Design Boot Camp, 2015. "https://simons.berkeley.edu/talks/daniel-marx-2015-09-03" (abstract, slides and archived video). Google Scholar
  43. Atsuki Nagao, Kazuhisa Seto, and Junichi Teruyama. A moderately exponential time algorithm for k-IBDD satisfiability. In Proceedings of the 14th International Symposium, on Algorithms and Data Structures (WADS), pages 554-565, 2015. Google Scholar
  44. Sergey Nurk. An O(2^0.4058 m) upper bound for circuit SAT. Technical report, PDMI, 2009. Google Scholar
  45. Igor Carboni Oliveira. Algorithms versus circuit lower bounds. Electronic Colloquium on Computational Complexity (ECCC), TR13-117, 2013. Google Scholar
  46. Ramamohan Paturi, Michael E. Saks, and Francis Zane. Exponential lower bounds for depth three boolean circuits. Computational Complexity, 9(1):1-15, 2000. Google Scholar
  47. Wolfgang J. Paul. A 2.5 n-lower bound on the combinational complexity of Boolean functions. SIAM J. Comput., 6(3):427-443, 1977. Google Scholar
  48. Anup Rao. Extractors for low-weight affine sources. In Proceedings of the 24th Annual IEEE Conference on Computational Complexity (CCC), pages 95-101, 2009. Google Scholar
  49. Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki, and Junichi Teruyama. Bounded depth circuits with weighted symmetric gates: Satisfiability, lower bounds and compression. In Proceedings of the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS), 2016, to appear. Google Scholar
  50. Rahul Santhanam. Circuit lower bounds for Merlin-Arthur classes. SIAM J. Comput., 39(3):1038-1061, 2009. Google Scholar
  51. Rahul Santhanam. Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In Proceedings of the 51th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 183-192, 2010. Google Scholar
  52. Rahul Santhanam. Ironic complicity: Satisfiability algorithms and circuit lower bounds. Bulletin of the EATCS, 106:31-52, 2012. Google Scholar
  53. Claus-Peter Schnorr. Zwei lineare untere schranken für die komplexität boolescher funktionen. Computing, 13(2):155-171, 1974. Google Scholar
  54. Kazuhisa Seto and Suguru Tamaki. A satisfiability algorithm and average-case hardness for formulas over the full binary basis. Computational Complexity, 22(2):245-274, 2013. Google Scholar
  55. Ronen Shaltiel. Dispersers for affine sources with sub-polynomial entropy. In Proceedings of the 52nd Annual IEEE Symposium on Foundations of Computer Science (FOCS), pages 247-256, 2011. Google Scholar
  56. Claude E. Shannon. The synthesis of two-terminal switching circuits. The Bell System Technical Journal, 28(1):59-98, 1949. Google Scholar
  57. Larry J. Stockmeyer. On the combinational complexity of certain symmetric Boolean functions. Mathematical Systems Theory, 10:323-336, 1977. Google Scholar
  58. Avishay Tal. #SAT algorithms from shrinkage. Electronic Colloquium on Computational Complexity (ECCC), TR15-114, 2015. Google Scholar
  59. Fengming Wang. NEXP does not have non-uniform quasipolynomial-size ACC circuits of o(loglogn) depth. In Proceedings of the 8th Annual Conference on Theory and Applications of Models of Computation (TAMC), pages 164-170, 2011. Google Scholar
  60. Ryan Williams. Improving exhaustive search implies superpolynomial lower bounds. SIAM J. Comput., 42(3):1218-1244, 2013. Google Scholar
  61. Ryan Williams. Natural proofs versus derandomization. In Proceedings of the 45th ACM Symposium on Theory of Computing Conference (STOC), pages 21-30, 2013. Google Scholar
  62. Ryan Williams. Algorithms for circuits and circuits for algorithms. In Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC), pages 248-261, 2014. Google Scholar
  63. Ryan Williams. New algorithms and lower bounds for circuits with linear threshold gates. In Proceedings of the 46th Symposium on Theory of Computing (STOC), pages 194-202, 2014. Google Scholar
  64. Ryan Williams. Nonuniform ACC circuit lower bounds. J. ACM, 61(1):2, 2014. Google Scholar
  65. Amir Yehudayoff. Affine extractors over prime fields. Combinatorica, 31(2):245-256, 2011. Google Scholar
  66. Uri Zwick. A 4n lower bound on the combinational complexity of certain symmetric Boolean functions over the basis of unate dyadic Boolean functions. SIAM J. Comput., 20(3):499-505, 1991. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact