Publications and Other Research
Sam Buss


Publication and research web page.  When possible, papers are available to download.
Warning:  These online versions may differ from the actual published versions (sometimes better, sometimes worse, than the published version).

My online CV also has a list of my publications — but usually there are more papers available below than are listed in my c.v.

For papers that are too recent to appear here, please email me, sbuss@ucsd.edu.

Copyright notice:  All material downloadable from this page is copyrighted by Sam Buss, his coauthors, and/or the publishers.

Publications.

Books (authored)

  1. Samuel R. Buss, 3D Computer Graphics: A Mathematical Introduction with OpenGL, Cambridge University Press, 2003.
  2. Samuel R. Buss, Bounded Arithmetic, Bibliopolis, Naples 1986.  221+v pages. Revision of 1985 Ph.D. thesis.

Books (edited)

  1. Samuel R. Buss, Petr Hájek and Pavel Pudlák (eds), Logic Colloquium '98, Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, held in Prague, Czech Republic, August 9-15, 1998, Lecture Notes in Logic 13, Association for Symbolic Logic, AK Peters, Natick, MA, 2000.   xvi+541 pages.
  2. Samuel R. Buss (ed.), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics #137, Elsevier, Amsterdam, 1998, x+811 pages.
  3. Paul Beame and Samuel R. Buss (eds.), Proof Complexity and Feasible Arithmetics, DIMACS Series in Discrete Mathematics and Theoretical Computer Science #39, American Mathematical Society, Providence, RI, 1998, xii+320 pages.
  4. Samuel R. Buss and Phillip J. Scott (eds.), Feasible Mathematics: A Mathematical Sciences Institute Workshop, Ithaca, New York June 1989, Progress in Computer Science #9, Birkhauser, Boston, 1990, viii+350 pages.

Software

  1. OpenGL Computer graphics software accompanying the book "3D Computer Graphics: A Mathematical Introduction with OpenGL". Also available:i Legacy versions of OpenGL software.
  2. Raytrace software, accompanying the same book.
  3. Inverse Kinematics demos, Jin-Su Kim). Associated article and unpublished survey are also available.
  4. Spherical Averages and Spherical Splines. Software for the Buss-Fillmore spherical averages algorithms.
  5. bussproofs.sty. The "Buss proofs" LaTeX/TeX style file for creating proof trees.
  6. qcmatch. Quasiconvex minimum-cost matching algorithm in ANSI C. (joint with D. Robinson, K. Kanzelberg, P. Yianilos). Associated article and technical report also available.
  7. StConn. Software for generating unsatisfiable CNFs based on the st-connectivity principle for planar grid graphs.
  8. FmlaChain. Software for generating unsatisfiable CNFs based on the equivalence chain and implication chain principles for Boolean formulas.
  9. TwoVertexBottlenecks. Software for finding all two vertex bottlenecks (TVBs) in a directed acyclic graph. This was developed for determining Dual Implication Points in a CDCL conflict graph.

Papers - journal articles and conference proceedings.

  1. (with Jonathan Chung, Vijay Ganesh and Albert Oliveras) Extended Resolution Clause Learning via Dual Implication Points, Preprint, March 2024.
  2. (with Oliver Kullmann and Virgina Vassilevska Williams) Dual Depth First Search for Binary Clause Reasoning, Preprint, March 2024.
  3. (with Vijay Ganesh and Albert Oliveras) A Linear Time Algorithm for Two-Vertex Bottlenecks, Preprint and software, March 2024.
  4. (with Emre Yolcu) Regular Resolution Effectively Simulates Resolution", Information Processing Letters, to appear, 2024.
  5. (with Neil Thapen) A Simple Supercritical Tradeoff between Size and Height in Resolution, Submitted. December 2023.
  6. Polynomially Verifiable Arithmetic, in Logic, Automata, and Computational Conplexity: The Works of Stephen A. Cook, ACM Press, 2023, 95-106.
  7. (with Albert Atserias and Moritz Müller) On the Consistency of Circuit Lower Bounds for Non-Deterministic Time, in Proceedings 55th ACM Symposium on Theory of Computing (STOC), 2023, pp. 1257-1270.
  8. (with Noah Fleming, and Russell Impagliazzo} TFNP Characterizations of Proof Systems and Monotone Circuits, in Innovations in Theoretical Computer Science (ITCS), LIPIcs 251, 2023, 30:1-30:40.
  9. (with Maria Luisa Bonet, Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva) Propositional Proof Systems Based on Maximum Satisfiability, Artificial Intelligence 300 (2021) 103552.
  10. (with Neil Thapen) DRAT and Propagation Redundancy Without New Variables, Logical Methods of Computer Science 17, 2 (2021) 12:1-31.
  11. Substitution and Propositional Proof Complexity, in Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs, Springer Verlag, 2022, pp. 477-496.
  12. (with Dmitry Itsykson, Alexander Knop, Artur Riazanov, and Dmitry Sokolov) Lower Bounds on OBDD Proofs with Several Orders, ACM Transactions on Computational Logic 22, 4, Article 26 (2021) 30 pages.
  13. (with Anupam Das and Alexander Knop) Proof Complexity of (Non-deterministic) Decison Trees and Branching Programs, in Proceeedings 28th Conference on Computer Science Logic (CSL), LIPIcs 137 (2020), 12:1-12:17.
  14. (with Jakob Nordström) Proof Complexity, in: Handbook of Satisfiability, 2nd Edition, 2021.
  15. (with Neil Thapen) DRAT Proofs, Propagation Redundancy, and Extended Resolution, in Proceedings, Theory and Applications of Satisfiability Testing (SAT 2019), July 2019.
  16. (with David L. Freese, Peter D. Olcott, and Craig S. Levin) GRAY: A Ray_Tracing based Monte-Carlo simulator for PET, Physics in Biology and Medicine 63 (2018) 105019, 14pp.
  17. (with Alexander Knop, Dmitry Itsykson, and Dmitry Sokolov) Reordering Rule Makes OBDD Proof Systems Stronger, in Proc. 33rd Computational Complexity Conference (CCC), 2018, pages 16:1-24.
  18. (with Alexander Knop) Strategies for Stable Merge Sorting, preprint, December 2017.
  19. (with Arnold Beckmann) On Transformations of Constant Depth Propositional Proofs, Annals of Pure and Applied Logic, 170, 10 (2019) 1176-1187.
  20. (with Maria Luisa Bonet, Alexey Ignatiev, Joao Marques-Silva, and Antonio Morgado) MaxSAT Resolution with the Dual Rail Encoding, in Proceedings, AAAI Conference on Artifical Intelligence (AAAI'18), April 2018.
  21. (with Ramyaa) Short Refutations for the Equivalence-Chain Principle for Constant-Depth Formulas, Mathematical Logic Quarterly 64, 6 (2018) 505-513.
  22. (with Jan Johannsen) On Linear Resolution, Journal of Satisfiability, Boolean Modeling and Computation 10 (2016) 23-35.
  23. (with Arnold Beckmann, Sy-David Friedman, Moritz Müller and Neil Thapen) Feasible Set Functions have Small Circuits, Computability 8, 1 (2019) 67-98.
  24. (with Valentine Kabanets, Antonina Kolokolova and Michal Koucký) Expander Construction in VNC1. Annals of Pure and Applied Logic 171, 7 (2020) Article 102796 (40 pages). Extended abstract in Proceedings, 8th Conference on Innovations in Theoretical Computer Science (ITCS'2017).
  25. (with Arnold Beckmann) The NP Search Problems of Frege and Extended Frege Proofs. ACM Transactions on Computational Logic, 18, 2 (2017) Article 11.
  26. (with Arnold Beckmann, Sy-David Friedman, Moritz Müller and Neil Thapen) Cobham Recursive Set Functions and Weak Set Theories. In Sets and Computations, World Scientific Publishing, 2018, pp. 55-116.
  27. (with Douglas Cenzer, Mia Minnes, and Jeffrey B. Remmel) Injection Structures Specified by Finite State Transducers. Computability and Complexity, Lecture Notes in Computer Science #10010, Springer Verlag, 2016, pp. 394-417.
  28. (with James Aisenberg and Maria Luisa Bonet). 2-D Tucker is PPA Complete, Journal of Computer and System Sciences, 108 (2020) 92-103.
  29. Uniform Proofs of ACC Representations, Archive for Mathematical Logic 56, 5-6 (2017) 639-669.
  30. Propositional Proofs in Frege and Extended Frege Systems (Abstract). Proceedings of the 10th International Computer Science Symposium in Russia (CSR). Lecture Notes in Computer Science 9139. Springer-Verlag, Lecture Notes in Computer Science 9139, 2015, pp. 1-6.
  31. (with James Aisenberg, Maria Luisa Bonet, Adrian Crãciun, and Gabriel Istrate). Short Proofs of the Kneser-Lovász Coloring Principle. Information and Computation 261, 2 (2018) 296-310. Earlier verson appeared in Proceedings of the 42nd International Colloquium on Automata, Languages and Programming (ICALP), Springer-Verlag Lecture Notes in Computer Science 9135, 2015. pp. 44-55.
  32. (with Arnold Beckmann, Sy David Friedman, Moritz Müller, and Neil Thapen). Cobham Recursive Set Functions, Annals of Pure and Applied Logic 167, 3 (2016) 335-369.
  33. Quasipolynomial Size Proofs of the Propositional Pigeonhole Principle. Theoretical Computer Science 576, C (2015) 77-84. DOI: 10.1016/j.tcs.2015.02.005.
  34. (with James Aisenberg and Maria Luisa Bonet). Quasipolynomial Size Proofs of Frankl's Theorem on the Trace of Sets, Journal of Symbolic Logic 81, 2 (2016) 1-24.
  35. (with Douglas Cenzer and Jeffrey B. Remmel). Sub-computable Bounded Randomness, Logical Methods of Computer Science, 10, 4 (2014) paper 15.
  36. Alternation-Trading Proofs and Their Limitations. Proc. 38th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS 2013), Lecture Notes in Computer Science 8087, Springer-Verlag, pp. 1-7,
  37. (with Michael Soltys). Unshuffling a Square is NP-Hard. Journal of Computer and System Sciences, 80, 4 (2014) 766-776.
  38. (with Leszek Kołodziejczyk). Small Stone in Pool. Logical Methods of Computer Science 10, 2 (2014) paper 16.
  39. (with Maria Luisa Bonet and Jan Johannsen). Improved Separations of Regular Resolution from Clause Learning Proof Systems. Journal of Artifical Intelligence Research 49 (2014) 669-703.
  40. (with Arnold Beckmann and Sy Friedman). Safe Recursive Set Functions. Journal of Symbolic Logic 80, 3 (2015) 730-762.
  41. (with Leszek Kołodziejczyk and Konrad Zdanowski). Collapsing Modular Counting in Bounded Arithmetic and Constant Depth Propositional Proofs. Transactions of the American Mathematical Society 367 (2015) 7517-7563.
  42. (with Mia Minnes). Probabilistic Algorithmic Randomness. Journal of Symbolic Logic 78, 2 (2013) 579-601.
  43. (with Arnold Beckmann). Improved Witnessing and Local Improvement Principles for Second-Order Bounded Arithmetic. ACM Transactions on Computational Logic 15, 1 (2014) Article 2, 35 pages.
  44. (with Leszek Kołodziejczyk and Neil Thapen). Fragments of Approximate Counting. Journal of Symbolic Logic 49 (2014) 496-525.
  45. Cut Elimination In Situ. In Gentzen's Centenary: The Quest for Consistency, R. Kahle and M. Rathjen, eds., Springer Verlag, 2015, pages 245-277.
  46. (with Maria Luisa Bonet). An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. In Theory and Applications of Satisfiability Testing (SAT 2012), Springer-Verlag Lecture Notes in Computer Science 7317, pp. 44-57, 2012. An extended abstract is available as: M.L. Bonet, S. Buss, An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract) 23rd International Joint Conference on Artificial Intelligence (IJCAI'13), pp.\ 2972-2976, 2013.
  47. (with Ryan Williams). Limits on Alternation-Trading Proofs for Time-Space Lower Bounds. Computational Complexity 24, 3 (2015) 533-600. Earlier conference version appeared in Proc. IEEE 27th Annual Conference on Computational Complexity (CCC), pp. 181-191, 2012.
  48. (with Alan Johnson). Propositional proofs and reductions between NP search problems. Annals of Pure and Applied Logic 163, 9 (2012) 1163-1182.
  49. (with Yijia Chen, Jörg Flum, Sy Friedman, and Moritz Müller). Strong isomorphism reductions in complexity theory. Journal of Symbolic Logic 76, 4 (2011) 1381-1402.
  50. Sharpened Lower Bounds for Cut Elimination. Journal of Symbolic Logic 77, 2 (2012) 656-668.
  51. (with Arnold Beckmann). Corrected Upper Bounds for Free-Cut Elimination. Theoretical Computer Science 412, 39 (2011) 5433-5445.
  52. (with Alan Johnson). The Quantifier Complexity of Polynomial-Size Iterated Definitions in First-Order Logic. Mathematical Logic Quarterly, 56, 6 (2010) 573-590.
  53. Towards NP-P via Proof Complexity and Search. Annals of Pure and Applied Logic 163, 7 (2012) 906-917. Also in: Foundational Adventures: Essays in Honor of Harvey Friedman, Templeton Foundation Press, Article 13, 2012. To appear.
  54. (with Arnold Beckmann). Characterizing Definable Search Problems in Bounded Arithmetic via Proof Notations. In Ways of Proof Theory, ONTOS Series in Mathematical Logic, pp. 65-134, 2010.
  55. (with Daniel Tracy and Bryan Woods). Efficient Large-Scale Sweep and Prune Methods with AABB Insertion and Removal. In: IEEE Virtual Reality (VR2009), pp. 191-198, 2009.
  56. (with Arnold Beckmann). Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic. Journal of Mathematical Logic 9, 1 (2009) 103-138.
  57. Pool Resolution is NP-hard to Recognize. Archive for Mathematical Logic 48, 8 (2009) 793-798.
  58. (with Roman Kuznets). Lower Complexity Bounds in Justification Logic. Annals of Pure and Applied Logic 163, 7 (2012) 888-905.
    Earlier conference proceedings version: The NP-Completeness of Reflected Fragments of Justification Logics. In Logical Foundations of Computer Science, LFCS'09, Springer-Verlag Lecture Notes in Computer Science #5407, 2009, pp. 122-136.
  59. (with Jan Hoffmann and Jan Johannsen). Resolution Trees with Lemmas - Resolution Refinements that Characterize DLL-Algorithms with Clause Learning. Logical Methods in Computer Science, 4, 4:13, 2008.
  60. (with Jan Hoffmann). The NP-hardness of Finding a Directed Acyclic Graph for Regular Resolution. Theoretical Computer Science 396 (2008) 271-276.
  61. The Computational Power of Bounded Arithmetic from the Predicative Viewpoint. In New Computational Paradigms, Changing Conceptions of What is Computable, edited by S.B. Cooper, B. Löwe, A. Sorbi, Springer, New York, 2008, pp. 213-222.
  62. (with Peter D. Olcott, Craig S. Levin, Guillem Pratx, and Chris K. Sramek). GRAY: High Energy Photon Ray Tracer for PET Applications, In 2006 IEEE Nuclear Science Symposium Conference Record, 2006, Volume 4, pp. 2011-2015.
  63. Nelson's Work on Logic and Foundations and Other Reflections on Foundations of Mathematics. In Diffusion, Quantum Theory, and Radically Elementary Mathematics, edited by W. Faris, Princeton University Press, 2006, pp. 183-208. Slides from a related talk also available.
  64. Bounded Arithmetic and Constant Depth Frege Proofs. In Complexity of Computations and Proofs, edited by J. Krajíček, Quaderni di Matematica, vol. 13, 2004, pp. 153-174.   Slides from a related conference presentation also available.
  65. (with Arnold Beckmann). Separation Results for the Size of Constant-depth Propositional Proofs. Annals of Pure and Applied Logic 136, no 1-2 (2005) 30-55.
  66. Collision Detection with Relative Screw Motion. The Visual Computer 21 (2005) 41-58.
  67. (with Jin-Su Kim). Selectively Damped Least Squares for Inverse Kinematics. Journal of Graphics Tools, 10, no.3 (2005) 37-49.
  68. (with Peter Clote). Solving the Fisher-Wright and coalescence problems with a discrete Markov chain analysis. Advances in Applied Probability 36, 4 (2004) 117-197.
  69. Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies. Theoretical Computer Science 357, no. 1-3, (2006) 35-52.
  70. (with Nate Segerlind and Russell Impagliazzo). A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM Journal on Computing 33, 5 (2004) 1171-1200. An earlier version appeared in the Proceedings of the 43rd Annual Symposium on Foundations of Computer Science (FOCS'02), IEEE Computer Society, 2002, pp. 604-613.
  71. Accurate and Efficient Simulations of Rigid Body Rotations. Journal of Computational Physics 164 (2000) 377-406.
  72. (with Alekos Kechris, Anand Pillay and Richard Shore). Prospects for Mathematical Logic in the Twenty-first Century, Journal of Symbolic Logic 7 (2001) 169-196.
  73. (with Bruce Kapron). Resource-bounded Continuity and Sequentiality for Type-two Functionals, ACM Transactions on Computational Logic 3 (2002) 402-417. Extended abstract appeared in Proceedings, 15th IEEE Symposium on Logic in Computer Science (LICS), 2000, pp. 77-83.
  74. (with Arnold Beckmann and Chris Pollett). Ordinal Notations and Well-orderings in Bounded Arithmetic, Annals of Pure and Applied Logic 120 (2002) 197-223. Publisher's erratum: Annals of Pure and Applied Logic 123 (2003) 291.
  75. (with Pavel Pudlák). On the Computational Content of Intuitionistic Propositional Proofs, Annals of Pure and Applied Logic 109 (2001) 49-64.
  76. (with Grigori Rosu). Incompleteness of Behavioral Logics, Proceedings, Coalgebraic Methods in Computer Science, CMCS'2000, Electronic Notes in Theoretical Computer Science 33 (2000) 61-69.
  77. (with Peter Yianilos). Linear and O(n log n) Time Minimum-cost Matching Algorithms for Quasiconvex Tours, SIAM Journal on Computing 27 (1998) 170-201. Expanded version of a paper which appeared in Proceedings of the Fifth ACM-SIAM Symposium on Discrete Algorithms (SODA), 1994, pp. 65-76. See also associated software and technical report.
  78. (with Dima Grigoriev, Russell Impagliazzo and Toniann Pitassi). Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes. Journal of Computer and System Sciences 62 (2001) 267-289. Earlier version in Proceedings, 31st Annual ACM Symposium on Theory of Computing (STOC'99), pp. 547-556. One page abstract in 14th IEEE Conference on Computational Complexity (CCC'99) p. 5-5.
  79. (with Jay Fillmore). Spherical Averages and Applications to Spherical Splines and Interpolation. ACM Transactions on Graphics 20 (2001) 95-126. Source code for a C++ implementation available too.
  80. (with Grigori Mints). The Complexity of the Disjunction and Existence Properties in Intuitionistic Logic. Pure and Applied Logic 99 (1999) 93-104.
  81. Propositional Proof Complexity: An Introduction. In Computational Logic, edited by U. Berger and H. Schwichtenberg, Springer-Verlag, Berlin, 1999, pp. 127-178.
  82. An Introduction to Proof Theory. In Handbook of Proof Theory, edited by S. Buss, Elsevier North-Holland, 1998, pp 1-78.
  83. First-order Proof Theory of Arithmetic. In Handbook of Proof Theory, edited by S. Buss, Elsevier North-Holland, 1998, pp 79-147.
  84. (with Misha Alekhnovich, Shlomo Moran and Toniann Pitassi). Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. Journal of Symbolic Logic 66 (2001) 171-191. An extended abstract appeared earlier in Mathematical Foundations of Computer Science (MFCS'98), Lecture Notes in Computer Science #1450, Springer-Verlag, 1998, pp. 176-184.
  85. Bounded Arithmetic, Proof Complexity and Two Papers of Parikh. Annals of Pure and Applied Logic 96 (1999) 43-55.
  86. Alogtime Algorithms for Tree Isomorphism, Comparison and Canonization. In Computational Logic and Proof Theory, Proceedings 5th Gödel Colloquium '97. Lecture Notes in Computer Science #1289, Springer-Verlag, Berlin, 1997, pp. 18-33.
  87. (with Toniann Pitassi). Resolution and the Weak Pigeonhole Principle. In Proceedings, Computer Science Logic (CSL'97), Lecture Notes in Computer Science #1414, Springer-Verlag, 1998, pp.149-156.
  88. Bounded Arithmetic and Propositional Proof Complexity. In Logic of Computation,, edited by H. Schwichtenberg, Springer-Verlag, Berlin, 1997, pp. 67-122.
  89. Lower Bounds on Nullstellensatz Proofs via Designs. In Proof Complexity and Feasible Arithmetics, edited by S. Buss and P. Beame, American Mathematical Society, Providence, RI, 1998, pp. 59-71.
  90. Bounded Arithmetic, Cryptography and Complexity. Theoria 63 (1997)147-167.
  91. (with Peter Clote). Cutting Planes, Connectivity and Threshold Logic. Archive for Mathematical Logic 35 (1996) 33-62.
  92. (with R. Impagliazzo, J. Krajíček, P. Pudlák, A. Razborov and J. Sgall). Proof Complexity in Algebraic Systems and Constant Depth Frege Systems with Modular Counting. Computational Complexity 6 (1995/1996) 256-298.
  93. (with Toniann Pitassi). Good Degree Bounds on Nullstellensatz Refutations of the Induction Principle. Journal of Computer and System Sciences 57 (1998) 162-171. Earlier version appeared in Complexity '96, Proceedings of the Eleventh Annual IEEE Conference on Computational Complexity, 1996, pp 233-242.
  94. (with Aleksandar Ignjatović). Unprovability of Consistency Statements in Fragments of Bounded Arithmetic. Annals of Pure and Applied Logic 74 (1995) 221-244.
  95. On Herbrand's Theorem. In Logic and Computational Complexity, Lecture Notes in Computer Science #960, 1995, Springer-Verlag, pp. 195-209.
  96. (with Pavel Pudlák). How To Lie Without Being (Easily) Convicted and Lengths of Proofs in Propositional Calculus. In Eighth Workshop on Computer Science Logic (CSL'94), Lecture Notes in Computer Science #933, Springer-Verlag, 1995, pp. 151-162.
  97. (with Maria Luisa Bonet and Toniann Pitassi). Are There Hard Examples for Frege Systems? In Feasible Mathematics II, Birkhauser, 1995, pp. 31-56.
  98. Relating the Bounded Arithmetic and Polynomial-Time Hierarchies. Annals of Pure and Applied Logic, 75 (1995) 67-77.
  99. (with Maria Luisa Bonet). Size-Depth Tradeoff for Boolean Formulae.. Information Processing Letters, 11 (1994) 151-155.
  100. Some Remarks on the Lengths of Propositional Proofs. Archive for Mathematical Logic 34 (1995) 377-394.
  101. On Gödel's Theorems on Lengths of Proofs I: Number of Lines and Speedups for Arithmetic. Journal of Symbolic Logic 39 (1994) 737-756.
  102. On Gödel's Theorems on Lengths of Proofs II: Lower Bounds for Recognizing k Symbol Provability. In Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.
  103. (with Maria Luisa Bonet). On the Serial Transitive Closure Problem. SIAM Journal on Computing 24 (1995) 109-122. See also next two items.
  104. (with Maria Luisa Bonet). The Deduction Rule and Linear and Near-Linear Proof Simulations. Journal of Symbolic Logic 58 (1993) 688-709. See also previous item and next item.
  105. (with Maria Luisa Bonet). On the Deduction Rule and the Number of Proof Lines In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science. (LICS'91). IEEE Computer Society Press, 1991, pp. 286-297. Subsumed by the previous two journal articles.
  106. The Witness Function Method and Provably Recursive Functions Of Peano Arithmetic. In Proceedings of Ninth International Congress on Logic, Methodology and Philosophy of Science, D. Prawitz, B. Skyrms and D. Westerstahl (eds), Elsevier Science North-Holland, 1994, pp. 29-68.
  107. Algorithms for Boolean Formula Evaluation and For Tree-Contraction. In Proof Theory, Complexity, and Arithmetic, P. Clote and J. Krajíček (eds), Oxford University Press, 1993, pp. 95-115.
  108. (with Jan Krajíček). An Application of Boolean Complexity to Separation Problems in Bounded Arithmetic. Proceedings of the London Mathematical Society 69 (1994) 1-21.
  109. (with Jan Krajíček and Gaisi Takeuti). Provably Total Functions in the Bounded Arithmetic Theories Ri3, Ui2, and Vi2. In Proof Theory, Arithmetic, and Complexity, P. Clote and J. Krajíček (eds), Oxford University Press, 1993, pp. 116-161.
  110. The Graph of Multiplication is Equivalent to Counting. Information Processing Letters 41 (1992) 199-201.
  111. (with Christos Papadimitriou and John Tsitsiklis). On the Predictability of Coupled Automata: an Allegory About Chaos. Complex Systems 5 (1991) 525-539. Earlier draft appeared in Proceedings of the 31st Annual Symposium on Foundations of Computer Science, volume II (FOCS' 1990), IEEE Computer Society Press, 1990, pp. 788-793.
  112. Intuitionistic Validity in T-normal Kripke Structures. Annals of Pure and Applied Logic 59 (1993) 159-173.
  113. On Model Theory for Intuitionstic Bounded Arithmetic with Applications to Independence. In Feasible Mathematics: A Mathematical Sciences Institute Workshop held in Ithaca, New York, June 1989. S. Buss and P. Scott (eds). Birkhauser,  1990, pp. 27-47.
  114. A Note on Bootstrapping Intuitionistic Bounded Arithmetic. In Proof Theory: a selection of papers from the Leeds Theory Programme 1990. P. Aczel, H. Simmons, S. Wainer (eds). Cambridge University Press, 1992, pp. 142-169.
  115. Propositional Consistency Proofs. Annals of Pure and Applied Logic 52 (1991) 3-29.
  116. The Undecidability of k-Provability. Annals of Pure and Applied Logic 53 (1991) 75-102.
  117. (with Louise Hay). On Truth-Table Reducibility to SAT. Information and Computation 91 (1991) 86-102.
  118. (with Louise Hay). On Truth-Table Reducibility to SAT and the Difference Hierarchy over NP. In Proceedings of the IEEE Structure in Complexity Conference. IEEE Computer Society Press, 1988, pp. 224-233.
  119. The Modal Logic of Pure Provability. Notre Dame Journal of Formal Logic 31 (1990) 225-231.
  120. (with Stephen A. Cook and Arvind Gupta and Vijaya Ramachandran). An Optimal Parallel Algorithm for Formula Evaluation. SIAM Journal on Computing 21(1992 755-780.
  121. (with Gyorgy Turan). Resolution Proofs of Generalized Pigeonhole Principles. Theoretical Computer Science 62 (1988) 311-317.
  122. Axiomatizations and Conservation Results for Fragments of Bounded Arithmetic. In Logic and Computation, Proceedings of a Workshop held at Carnegie Mellon University, June 30-July 2, 1987. AMS Contemporary Mathematics 106 (1990) 57-84.
  123. The Boolean Formula Value Problem is in ALOGTIME. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing (STOC), 1987, pp. 123-131.
  124. Polynomial Size Proofs of the Propositional Pigeonhole Principle. Journal of Symbolic Logic 52 (1987) 916-927.
  125. The Polynomial Hierarchy and Intuitionistic Bounded Arithmetic. In Structure in Complexity, Lecture Notes in Computer Science #223, Springer Verlag, 1986, pp. 77-103.
  126. A Conservation Result Concerning Bounded Theories and the Collection Axiom. Proceedings of the American Mathematic Society 100 (1987) 709-716.
  127. The Polynomial Hierarchy and Fragments of Bounded Arithmetic.. In Proceedings of the 17-th Annual ACM Symposium on Theory of Computing (STOC'85), 1985, pp. 285-290.
  128. (with P.N. Yianilos and R.A. Harbort). The Application of a Pattern Matching Algorithm to Searching Medical Record Text. In IEEE Symposium on Computer Applications in Medical Care, 1978, pp. 308-313.

Ph.D./Honors theses.

  1. Samuel R. Buss. Bounded Arithmetic. Ph.D. thesis, Department of Mathematics, Princeton University, 1985. 188+v pages.
  2. Samuel R. Buss. The Word Problem for Groups. Undergraduate Honors Thesis, Department of Mathematics, Emory University, 1979, 79 pages.

Reviews, unpublished articles and surveys, course lecture notes, and miscellaneous items.

  1. A review of Methods of Cut-Elimination by Matthias Baaz and Alexander Leitsch. Studia Logica, 103, 3 (2015) 663-667.
  2. A review of Forcing With Random Variables and Proof Complexity by Jan Krajíček. Bulletin of Symbolic Logic, 18,4 (2012) 576-578.
  3. (with Mia Minnes). Algorithmic Randomness with Probabilistic Strategies and Intermediate Success. Unpublished article. March 2013.
  4. Introduction to Inverse Kinematics with Jacobian Transpose, Pseudoinverse and Damped Least Squares methods. Unpublished survey article, 2004.
  5. (with Rosalie Iemhoff). The Depth of Intuitionistic Cut Free Proofs. Unpublished manuscript 2003.
  6. Student-written notes of my Math 267 - Propositional Proof Complexity course in Winter 2002.
  7. (with P. Yianilos). A Bipartite Matching Approach to Approximate String Comparison and Search. Unpublished manuscript.
  8. (with P. Yianilos). Secure Short-Key Cryptosystems: Forty Bits is Enough. Unpublished manuscript.
  9. Lectures on Proof Theory Technical Report number SOCS-96.1, School of Computer Science, McGill University, 1996, 117 pages.
  10. A review of the biography of K. Godel, Logical Dilemmas, by John Dawson. SIAM Review 40 (1998) 397-400.
  11. Student-written notes of my Math 267 - Mathematical Foundations of Cryptography course in Winter 1997.
  12. (with Peter Clote). Threshold logic proof systems. Unpublished manuscript. May 1995.
  13. (with D. Robinson, K. Kanzelberg, P. Yianilos). Solving the Minimum-Cost Matching Principle for Quasi-Convex Tours: An Efficient ANSI C Implementation. Technical report #370, Dept. of Computer Science Engineering, UCSD, April 1994, 69 pages. Associated software and journal article also available.
  14. A review of Exponential lower bounds for the pigeonhole principle by P. Beame, R. Impagliazzo, J Krajíček, T. Pitassi, P. Pudlák and A. Woods, in Computing Reviews 34 (May 1993) 261-261. Reprinted in SIGACT News 24 (1993) 41-41.
  15. Student-written notes of my Math 267 - Circuit Complexity course in Winter-Spring 1992.
  16. A review of three papers of Neil Immerman, Journal of Symbolic Logic 54 (1989) 287-288.
  17. (with S.A. Cook, P.W. Dymond and L. Hay). The log space oracle hierarchy collapses. Technical report #CS87-103. Computer Science Engineering Department, Univ. of California, San Diego, 1987.
  18. Student-written notes for Math 260A-C on Introduction to Mathematical Logic. Fall 1988-Spring 1989.
  19. Student-written notes of my Math 271 (Berkeley) topics course on Weak Formal Systems and Connections to Computational Complexity, Winter-Spring 1988.
  20. Neighborhood Metrics on n-Dimension Blocks of Characters, Technical report #00218-86, Mathematical Sciences Research Institute, Berkeley, California, September 1985.

Selected talks.

  1. Bounded Arithmetic and a Consistency Result for NEXP vs P/poly. Logic Seminar, Institute of Mathematics, Prague, Aplril 2024, and The Proof Society Workshop, Barcelona, June 2023.
  2. Some Challenge Problems for Resolution and One Also for AC0-Frege or:Seeking Hard Instances for Constant Depth Frege. Art of SAT, Shonan, Village, Japan, October 2, 2023.
  3. DRAT Proofs and Extensions: Satisfiability Solving with Conflict Driven Clause Learning and Non-implicational Inferences `University of Birmingham, June 15, 2023.
  4. On Extended Frege Proofs. ToniCS, Simons Institute, Berkeley, March 28, 2023.
  5. Gödel and Lengths of Proofs. Celebrating 90 Years of Gödel's Incompleteness Theorems, University of Tübingen, July 8, 2021.
  6. CDCL Solvers, Resolution, Extension and DRAT Proofs. Orevkov'80, 5th St. Peterburg Days in Logic and Computability, May 15, 2021.
  7. Proof Complexity Boot Camp. Slides for four pre-recorded videos and one live zoom presentation. Special Program in Satisfiability, Simons Institute, February 3, 2021.
  8. Propositional Branching Program Proofs and Logics for L and NL. Logic Seminar, Czech Academy of Sciences, Prague, November 14, 2020.
  9. Proof Complexity and Bounded Arithmetic. Four lectures, Caleidoscope Research School in Computational Complexity, Institut Henri Poincare, Paris, June 17-18, 2019.
  10. Totality, Provability, and Feasibility. Gödel Lecture, ASL Annual Meeting, CUNY, New York, May 22, 2019
  11. Bounded Arithmetic, Expanders and Monotone Propositional Proofs. Takeuti Symposium on Advances in Logic, Kobe, Japan, September 20, 2018.
  12. Introduction to Bounded Arithmetic, Workshop on Proof Complexity, St. Petersburg State University, May 15, 2016.
  13. Nonconstructive Proofs of Existence for Provably Total Search Problems. Presentation at Workshop on Theoretical Computer Science, Higher School of Economics, Moscow, April 2016.
  14. Nelson's Formalist Approach to Feasible Arithmetic and the Foundations of Mathematics. Presentation at American Philosophical Association, Western Division Meeting, San Francisco, March 2016.
  15. Provably Total Search Problems of Second-Order Bounded Arithmetic. Existence for Provably Total Search Problems Journes sur les Arithmetiques Faibles (JAF) and MAMLS, New York City, July 2015.
  16. On the Power of Diagonalization for Separating Complexity Classes, Yandex, Moscow, Russia, July 2015.
  17. Tutorial on Proof Systems Related to SAT Solvers, Workshop on Theory and Practice of SAT Solving, Dagstuhl, Germany, April 2015.
  18. Cobham recursion and polynomial time on sets. Workshop on Sets and Computations, Singapore, April 2015; Similar earlier talks at Oberwolfach, November 2014; Stanford University, October 2014; and Infinity Workshop, Summer of Logic, Vienna. July 2014.
  19. Complexity of Propositional Proofs: Some Theory and Examples UPC, Barcelona, April 2015 and Swansea University, March 2015.
  20. Search Problems, Proof Complexity, and Second-Order Bounded Arithmetic. Logic and Computational Complexity, Summer of Logic, Vienna. July 2014.
  21. Towards (Non-)Separations in Propositional Proof Complexity. Stanford University, February 2014.
  22. Mini-Tutorial on Proof Complexity. Workshop on Theoretical Foundations of SAT Solving. BIRS, Banff, Canada. January 2014.
  23. Collapsing Modular Counting in Bounded Arithmetic and Constant Depth Propositional Proofs. Limits of Theorem Proving (LiThPr). Rome, Italy, September 2012.
  24. An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning. Theory and Applications of Satisfiability Testing (SAT 2012). Trento, Italy, June 2012.
  25. Total NP Functions I: Complexity and Reducibility and Total NP Functions II: Provability and Reducibility. Two tutorial talks on NP Search. Workshop on Logical Approaches to Complexity II, Newton Institute, Cambridge, England, March 2012.
  26. Expressibility, and the Complexity of Proofs, PhilMath Intersem, Paris 7 Diderot, June 2011.
  27. Proof Complexity and the Complexity of SAT Solvers, First International SAT/SMT Solver Workshop, Boston, June 2011.
  28. Limits on Alternation-Trading Proofs for Time-Space Bounds for Satisfiability, Barcelona, February 2011; Wales, March 2011; Paris, June 2011.
  29. SAT Solver Trials: Experiments with a SAT Solver, Infinity Project, Centre de Recerca Matemàtica, Barcelona, Spain, December 2009.
  30. A series of four talks on NP Functions, Local Search, and Bounded Arithmetic, Prague Fall School on Logic and Complexity, September 2009.
  31. Towards NP-P and Satisfiability via Proof Complexity and Proof Search, Logical Foundations of Computer Science (LFCS'09), January 2009.
  32. The NP-Completeness of Reflected Fragments of Justification Logics, Logical Foundations of Computer Science (LFCS'09), January 2009.
  33. Polynomial Local Search higher in the Polynomial Hierachy and Bounded Arithmetic, BIRS Workshop on Computability, Reverse Mathematics and Combinatorics, Banff, Canada, December 2008. Also at Research Workshop on Proof Theory and Constructivity, Leeds, July 2009.
  34. Large Numbers, Busy Beavers, Noncomputability and Incompleteness, Food for Thought seminar, UCSD, November 2007.
  35. The Computational Power of Bounded Arithmetic from the Predicative Viewpoint, ASL Winter Meeting, special session, January 2007.
  36. Propositional Proof Systems and Search, Connections II: Fundamentals of Network Science, Caltech, August 2006.
  37. Proof Complexity and Computational Hardness, Computability in Europe (CiE), July 2006, Swansea, Wales. Three tutorial lectures.
  38. Bounded Arithmetic, Constant-Depth Proofs and st-Connectivity. UCLA Logic Meeting (VIG), February 2004. Contains st-Connectivity and Hex tautology work.
  39. Ed Nelson's Work on Logic and Foundations: Radical Constructivism. Presentation at Workshop on Analysis, Probability and Logic, Pacific Institute of Mathematical Studies (PIMS), UBC, Vancouver, June 2004. A related paper is also available.
  40. Is It Easier To "Discover" Than To "Verify"?. UCSD Math Circle presentation to high school students. May 22, 2004.
  41. Bounded Arithmetic and Bounded Depth Propositional Proofs. Takeuti Symposium on Mathematical Logic. Kobe, Japan, December, 2003.
  42. Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies Workshop on Proof Theory, Muenster, October 2003; and 12th Latin American Symposium on Mathematical Logic (SLALM), Costa Rica, January 2004.
  43. Spherical Splines and Applications to Spherical Splines and Interpolation. Pixel Cafe, UCSD, December 2002.
  44. Taylor series methods for rigid body simulation and extensions to Lie groups. Seventh SIAM Conference on Geometric Design and Computing. Sacramento. November 2001.
  45. Bounded arithmetic and propositional proofs. NATO International Summer School on Logic of Computation. Marktoberdorf, Germany. July-August 1995. Five hours of lectures.

Selected Ph.D. dissertations by students. (More can be available upon request.)

  1. David Robinson, Parallel Algorithms for Group Word Problems, Ph.D. Thesis, Department of Mathematics, University of Califoria, San Diego, 1993.
  2. Nathan Segerlind, New Separations in Propositional Proof Complexity, Ph.D. Thesis, Department of Mathematics, University of Califoria, San Diego, 2003.

Acknowledgements. The bulk of the above work on this page was performed with partial financial support under various NSF grants.   Some parts of the above work were funded in part by grants from NATO and from the Czech Academy of Sciences and from the Simons Foundation.

Patents

  1. Peter N. Yianilos and Samuel R. Buss, Associative Memory Circuit System and Method, continuation in part, U.S. Patent #4490811, December 1984.  European patent #83903352.9, January 1986.
  2. Samuel R. Buss and Peter N. Yianilos, Linear and Non-linear Time Methods for Minimum Cost Matching on Quasiconvex Tours, U.S. Patent #5841958, November 1998.

Computer games. Computer games with algorithms or code by Buss. See also my Moby Games rap sheet at http://www.mobygames.com/developer/sheet/view/developerId,42330/ (This lists only games with explicit credit given, not all the games that use Buss's algorithms and code.)

  1. Grand Theft Auto: Episodes from Liberty City., Rockstar Games, 2010.
  2. Grand Theft Auto IV: The Lost and Damned., Rockstar Games, 2010.
  3. Grand Theft Auto: The Ballad of Gay Tony., Rockstar Games, 2010.
  4. Grand Theft Auto IV, Rockstar Games, 2008.
  5. Smuggler's Run: Warzones, Rockstar Games, 2002.
  6. TransWorld SURF, Infogames, 2002.
  7. Smuggler's Run 2: Hostile Territory, Rockstar Games, 2001.
  8. Midnight Club: Street Racing, Rockstar Games, 2000.
  9. Midtown Madness 2, Microsoft Game Studios, 2000.
  10. Smuggler's Run, Rockstar Games, 2000.
  11. Midtown Madness, Microsoft Game Studios, 1999.