Applying practice to theory

ABSTRACT

How can complexity theory and algorithms benefit from practical advances in computing? We give an overview of some prior work using practical computing to attack problems in computational complexity and algorithms, informally describe how linear program solvers may be used to help prove new lower bounds for satisfiability, and suggest a research program for developing new understanding in circuit complexity.

REFERENCES

• 1: Michael Alekhnovich , Allan Borodin , Joshua Buresh-Oppenheim , Russell Impagliazzo , Avner Magen , Toniann Pitassi, Toward a Model for Backtracking and Dynamic Programming, Proceedings of the 20th Annual IEEE Conference on Computational Complexity, p.308-322, June 11-15, 2005 [doi>10.1109/CCC.2005.32]
• 2: K. Appel and W. Haken. Every planar map is four colorable. Part I. Discharging. Illinois J. Math. 21:429--490, 1977.
• 3: K. Appel, W. Haken, and J. Koch. Every planar map is four colorable. Part II. Reducibility. Illinois J. Math. 21:491--567, 1977.
• 4: Sanjeev Arora , Shmuel Safra, Probabilistic checking of proofs: a new characterization of NP, Journal of the ACM (JACM), v.45 n.1, p.70-122, Jan. 1998 [doi>10.1145/273865.273901]
• 5: Sanjeev Arora , Carsten Lund , Rajeev Motwani , Madhu Sudan , Mario Szegedy, Proof verification and the hardness of approximation problems, Journal of the ACM (JACM), v.45 n.3, p.501-555, May 1998 [doi>10.1145/278298.278306]
• 6: Mihir Bellare , Oded Goldreich , Madhu Sudan, Free Bits, PCPs, and Nonapproximability---Towards Tight Results, SIAM Journal on Computing, v.27 n.3, p.804-915, June 1998 [doi>10.1137/S0097539796302531]
• 7: M. Benedetti. sKizzo: A suite to evaluate and certify QBFs. Proc. Int'l Conf. on Automated Deduction, 369--376, 2005.
• 8: Nader H. Bshouty , Richard Cleve , Ricard Gavaldà , Sampath Kannan , Christino Tamon, Oracles and queries that are sufficient for exact learning, Journal of Computer and System Sciences, v.52 n.3, p.421-433, June 1996 [doi>10.1006/jcss.1996.0032]
• 9: Stephen A. Cook, A hierarchy for nondeterministic time complexity, Proceedings of the fourth annual ACM symposium on Theory of computing, p.187-192, May 01-03, 1972, Denver, Colorado, United States [doi>10.1145/800152.804913]
• 10: Stephen A. Cook, Short propositional formulas represent nondeterministic computations, Information Processing Letters, v.26 n.5, p.269-270, Jan. 11, 1988 [doi>10.1016/0020-0190(88)90152-4]
• 11: David Eppstein, Quasiconvex analysis of multivariate recurrence equations for backtracking algorithms, ACM Transactions on Algorithms (TALG), v.2 n.4, p.492-509, October 2006 [doi>10.1145/1198513.1198515]
• 12: S.S. Fedin and A.S. Kulikov. Automated proofs of upper bounds on the running time of splitting algorithms. J. Math. Sciences 134(5):2383--2391, 2006.
• 13: F.V. Fomin, F. Grandoni, and D. Kratsch. Measure and conquer: domination - a case study. Proc. ICALP, 191--203, 2005.
• 14: F.V. Fomin, F. Grandoni, and D. Kratsch. Some new techniques in design and analysis of exact (exponential) algorithms. Bulletin of the EATCS 87:47--77, 2005.
• 15: Fedor V. Fomin , Fabrizio Grandoni , Dieter Kratsch, Measure and conquer: a simple O(2^0.288n) independent set algorithm, Proceedings of the seventeenth annual ACM-SIAM symposium on Discrete algorithm, p.18-25, January 22-26, 2006, Miami, Florida [doi>10.1145/1109557.1109560]
• 16: Lance Fortnow , Richard Lipton , Dieter van Melkebeek , Anastasios Viglas, Time-space lower bounds for satisfiability, Journal of the ACM (JACM), v.52 n.6, p.835-865, November 2005 [doi>10.1145/1101821.1101822]
• 17: M. Garey, D. Johnson, and L. Stockmeyer. Some simplified NP-complete graph problems. Theor. Comput. Sci. 1:237--267, 1976.
• 18: Michel X. Goemans , David P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM (JACM), v.42 n.6, p.1115-1145, Nov. 1995 [doi>10.1145/227683.227684]
• 19: Jens Gramm , Jiong Guo , Falk Hüffner , Rolf Niedermeier, Automated Generation of Search Tree Algorithms for Hard Graph Modification Problems, Algorithmica, v.39 n.4, p.321-347, May 2004 [doi>10.1007/s00453-004-1090-5]
• 20: T.C. Hales. A proof of the Kepler conjecture. Annals of Math. 162:1065--1185, 2005.
• 21: J. Hass and R. Schlafly. Double bubbles minimize. Annals of Math. 151:459--515, 2000.
• 22: Johan Håstad, Some optimal inapproximability results, Journal of the ACM (JACM), v.48 n.4, p.798-859, July 2001 [doi>10.1145/502090.502098]
• 23: Kazuo Iwama , Hiroki Morizumi, An Explicit Lower Bound of 5n - o(n) for Boolean Circuits, Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science, p.353-364, August 26-30, 2002
• 24: Kazuo Iwama , Suguru Tamaki, Improved upper bounds for 3-SAT, Proceedings of the fifteenth annual ACM-SIAM symposium on Discrete algorithms, January 11-14, 2004, New Orleans, Louisiana
• 25: R. Kannan. Towards separating nondeterminism from determinism. Mathematical Systems Theory 17(1):29--45, 1984.
• 26: Howard Karloff , Uri Zwick, A 7/8-Approximation Algorithm for MAX 3SAT?, Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97), p.406, October 19-22, 1997
• 27: Arist Kojevnikov , Alexander S. Kulikov, A new approach to proving upper bounds for MAX-2-SAT, Proceedings of the seventeenth annual ACM-SIAM symposium on Discrete algorithm, p.11-17, January 22-26, 2006, Miami, Florida [doi>10.1145/1109557.1109559]
• 28: Oded Lachish , Ran Raz, Explicit lower bound of 4.5n - o(n) for boolena circuits, Proceedings of the thirty-third annual ACM symposium on Theory of computing, p.399-408, July 2001, Hersonissos, Greece [doi>10.1145/380752.380832]
• 29: C.W.H. Lam, L. Thiel, and S. Swiercz. The nonexistence of finite projective planes of order 10. Canad. J. Math. 41:1117--1123, 1989.
• 30: William McCune, Solution of the Robbins Problem, Journal of Automated Reasoning, v.19 n.3, p.263-276, December 1997 [doi>10.1023/A:1005843212881]
• 31: D. van Melkebeek. Time-space lower bounds for NP-complete problems. In Current Trends in Theoretical Computer Science 265--291, World Scientific, 2004.
• 32: Dieter van Melkebeek, A survey of lower bounds for satisfiability and related problems, Foundations and Trends® in Theoretical Computer Science, v.2 n.3, p.197-303, January 2006 [doi>10.1561/0400000012]
• 33: S.I. Nikolenko and A.V. Sirotkin. Worst-case upper bounds for SAT: automated proof. Proc. ESSLLI 225--232, 2003. URL: http://logic.pdmi.ras.ru/~sergey/
• 34: Neil Robertson , Daniel Sanders , Paul Seymour , Robin Thomas, The four-colour theorem, Journal of Combinatorial Theory Series B, v.70 n.1, p.2-44, May 1997 [doi>10.1006/jctb.1997.1750]
• 35: M. Robson. Finding a maximum independent set in time O (2^n/4). Technical Report 1251-01, LaBRI, Université de Bordeaux I, 2001. URL: http://www.labri.fr/perso/robson/mis/techrep.html
• 36: W.J. Savitch. Relationships between nondeterministic and deterministic tape classes. J. Comp. Sys. Sci. 4:177--192, 1970.
• 37: C. P. Schnorr, Satisfiability Is Quasilinear Complete in NQL, Journal of the ACM (JACM), v.25 n.1, p.136-145, Jan. 1978 [doi>10.1145/322047.322060]
• 38: A.D. Scott and G.B. Sorkin. Linear-programming design and analysis of fast algorithms for Max 2-CSP. Discr. Optimization 4(3-4):260--287, 2007.
• 39: N.J.A. Sloane and S. Plouffe. The encyclopedia of integer sequences. Academic Press, 1995.
• 40: V. Strassen. Gaussian elimination is not optimal. Numer. Math. 13:354--356, 1969.
• 41: Luca Trevisan , Gregory B. Sorkin , Madhu Sudan , David P. Williamson, Gadgets, Approximation, and Linear Programming, SIAM Journal on Computing, v.29 n.6, p.2074-2097, April 2000 [doi>10.1137/S0097539797328847]
• 42: R. Ryan Williams, Time-Space Tradeoffs for Counting NP Solutions Modulo Integers, Computational Complexity, v.17 n.2, p.179-219, May 2008 [doi>10.1007/s00037-008-0248-y]
• 43: R. Williams. Automated proofs of time lower bounds. Manuscript available at http://www.cs.cmu.edu/~ryanw/projects.html.
• 44: Uri Zwick, Computer assisted proof of optimal approximability results, Proceedings of the thirteenth annual ACM-SIAM symposium on Discrete algorithms, p.496-505, January 06-08, 2002, San Francisco, California

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.0 General

General Terms:
Algorithms, Design, Theory