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)

Samuel R. Buss,
3D Computer Graphics:
A Mathematical Introduction with OpenGL,
Cambridge University Press, 2003.

Samuel R. Buss, Bounded Arithmetic,
Bibliopolis, Naples 1986. 221+v pages.
Revision of 1985 Ph.D. thesis.
Books (edited)

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 915, 1998,
Lecture Notes in Logic 13,
Association for Symbolic Logic, AK Peters, Natick, MA, 2000.
xvi+541 pages.

Samuel R. Buss (ed.),
Handbook of
Proof Theory,
Studies in Logic and the Foundations of Mathematics #137,
Elsevier, Amsterdam, 1998, x+811 pages.

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.

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

OpenGL
Computer graphics software
accompanying the book
"3D Computer Graphics: A Mathematical Introduction with OpenGL".
Also available:i
Legacy versions of OpenGL software.

Raytrace
software,
accompanying the same book.

Inverse Kinematics demos,
JinSu Kim).
Associated article and unpublished survey are also available.

Spherical Averages and Spherical Splines.
Software for the BussFillmore spherical averages algorithms.

bussproofs.sty.
The "Buss proofs" LaTeX/TeX style file for creating proof trees.

qcmatch.
Quasiconvex minimumcost matching algorithm in ANSI C.
(joint with D. Robinson, K. Kanzelberg, P. Yianilos).
Associated article and technical report also available.

StConn. Software for generating
unsatisfiable CNFs based on the stconnectivity principle
for planar grid graphs.

FmlaChain. Software for generating
unsatisfiable CNFs based on the equivalence
chain and implication chain principles
for Boolean formulas.

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.

(with Jonathan Chung, Vijay Ganesh and Albert Oliveras)
Extended Resolution
Clause Learning via Dual Implication Points,
Preprint, March 2024.

(with Oliver Kullmann)
Dual Depth First Search for
Binary Clause Reasoning,
Preprint, March 2024.

(with Vijay Ganesh and Albert Oliveras)
A Linear Time Algorithm for
TwoVertex Bottlenecks,
Preprint and software, March 2024.

(with Emre Yolcu)
Regular Resolution Effectively
Simulates Resolution",
Information Processing Letters, to appear, 2024.

(with Neil Thapen)
A Simple Supercritical Tradeoff
between Size and Height in Resolution,
Submitted. December 2023.

Polynomially Verifiable Arithmetic,
in Logic, Automata, and Computational Conplexity:
The Works of Stephen A. Cook,
ACM Press, 2023, 95106.

(with Albert Atserias and Moritz Müller)
On the Consistency of
Circuit Lower Bounds for NonDeterministic Time,
in Proceedings 55th ACM Symposium on Theory of Computing (STOC),
2023, pp. 12571270.

(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:130:40.

(with Maria Luisa Bonet, Alexey Ignatiev, Antonio Morgado, Joao MarquesSilva)
Propositional Proof Systems Based on
Maximum Satisfiability,
Artificial Intelligence 300 (2021) 103552.

(with Neil Thapen)
DRAT and Propagation Redundancy
Without New Variables,
Logical Methods of Computer Science 17, 2 (2021) 12:131.

Substitution
and Propositional Proof Complexity,
in Alasdair Urquhart on Nonclassical and Algebraic Logic
and Complexity of Proofs,
Springer Verlag, 2022, pp. 477496.

(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.

(with Anupam Das and Alexander Knop)
Proof Complexity
of (Nondeterministic) Decison Trees and Branching Programs,
in Proceeedings 28th Conference on Computer Science Logic (CSL),
LIPIcs 137 (2020), 12:112:17.

(with Jakob Nordström)
Proof Complexity,
in: Handbook of Satisfiability, 2nd Edition, 2021.

(with Neil Thapen)
DRAT Proofs, Propagation Redundancy,
and Extended Resolution,
in Proceedings,
Theory and Applications of Satisfiability Testing (SAT 2019),
July 2019.

(with David L. Freese, Peter D. Olcott, and Craig S. Levin)
GRAY: A Ray_Tracing based MonteCarlo simulator
for PET,
Physics in Biology and Medicine 63 (2018) 105019, 14pp.

(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:124.

(with Alexander Knop)
Strategies for Stable Merge Sorting,
preprint, December 2017.

(with Arnold Beckmann)
On Transformations of Constant Depth
Propositional Proofs,
Annals of Pure and Applied Logic, 170, 10 (2019) 11761187.

(with Maria Luisa Bonet, Alexey Ignatiev, Joao MarquesSilva,
and Antonio Morgado)
MaxSAT Resolution
with the Dual Rail Encoding,
in Proceedings, AAAI Conference on Artifical Intelligence
(AAAI'18), April 2018.

(with Ramyaa)
Short Refutations for the EquivalenceChain
Principle for ConstantDepth Formulas,
Mathematical Logic Quarterly 64, 6 (2018) 505513.

(with Jan Johannsen)
On Linear Resolution,
Journal of Satisfiability, Boolean Modeling and Computation
10 (2016) 2335.

(with Arnold Beckmann, SyDavid Friedman, Moritz Müller and Neil Thapen)
Feasible Set Functions have
Small Circuits,
Computability 8, 1 (2019) 6798.

(with Valentine Kabanets, Antonina Kolokolova and Michal Koucký)
Expander Construction in VNC^{1}.
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).

(with Arnold Beckmann)
The NP Search Problems of
Frege and Extended Frege Proofs.
ACM Transactions on Computational Logic, 18, 2 (2017) Article 11.

(with Arnold Beckmann, SyDavid Friedman, Moritz Müller and Neil Thapen)
Cobham Recursive Set Functions
and Weak Set Theories.
In Sets and Computations,
World Scientific Publishing, 2018, pp. 55116.

(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. 394417.

(with James Aisenberg and Maria Luisa Bonet).
2D Tucker is PPA Complete,
Journal of Computer and System Sciences, 108 (2020) 92103.

Uniform Proofs of ACC Representations,
Archive for Mathematical Logic 56, 56 (2017) 639669.

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.
SpringerVerlag, Lecture Notes in Computer Science 9139,
2015, pp. 16.

(with James Aisenberg, Maria Luisa Bonet,
Adrian Crãciun, and Gabriel Istrate).
Short Proofs of the KneserLovász
Coloring Principle.
Information and Computation 261, 2 (2018) 296310.
Earlier verson appeared
in Proceedings of the 42nd International Colloquium on
Automata, Languages and Programming (ICALP),
SpringerVerlag Lecture Notes in Computer Science 9135,
2015.
pp. 4455.

(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) 335369.

Quasipolynomial Size Proofs of
the Propositional Pigeonhole Principle.
Theoretical Computer Science 576, C (2015) 7784.
DOI: 10.1016/j.tcs.2015.02.005.

(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) 124.

(with Douglas Cenzer and Jeffrey B. Remmel).
Subcomputable
Bounded Randomness,
Logical Methods of Computer Science, 10, 4 (2014) paper 15.

AlternationTrading Proofs
and Their Limitations.
Proc. 38th Intl. Symp. on Mathematical Foundations of Computer Science
(MFCS 2013),
Lecture Notes in Computer Science 8087,
SpringerVerlag, pp. 17,

(with Michael Soltys).
Unshuffling a Square is NPHard.
Journal of Computer and System Sciences, 80, 4 (2014) 766776.

(with Leszek Kołodziejczyk).
Small Stone in Pool.
Logical Methods of Computer Science 10, 2 (2014) paper 16.

(with Maria Luisa Bonet and Jan Johannsen).
Improved Separations of Regular Resolution
from Clause Learning Proof Systems.
Journal of Artifical Intelligence Research 49 (2014) 669703.

(with Arnold Beckmann and Sy Friedman).
Safe Recursive Set Functions.
Journal of Symbolic Logic 80, 3 (2015) 730762.

(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) 75177563.

(with Mia Minnes).
Probabilistic Algorithmic
Randomness.
Journal of Symbolic Logic 78, 2 (2013) 579601.

(with Arnold Beckmann).
Improved Witnessing and
Local Improvement Principles for SecondOrder
Bounded Arithmetic.
ACM Transactions on Computational Logic 15, 1 (2014) Article 2, 35 pages.

(with Leszek Kołodziejczyk and Neil Thapen).
Fragments of Approximate Counting.
Journal of Symbolic Logic 49 (2014) 496525.

Cut Elimination In Situ.
In Gentzen's Centenary: The Quest for Consistency,
R. Kahle and M. Rathjen, eds.,
Springer Verlag, 2015, pages 245277.

(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),
SpringerVerlag Lecture Notes in Computer Science 7317,
pp. 4457, 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.\ 29722976, 2013.

(with Ryan Williams).
Limits on AlternationTrading Proofs
for TimeSpace Lower Bounds.
Computational Complexity 24, 3 (2015) 533600.
Earlier conference version appeared in
Proc. IEEE 27th Annual Conference on Computational Complexity
(CCC),
pp. 181191, 2012.

(with Alan Johnson).
Propositional proofs and reductions between NP
search problems.
Annals of Pure and Applied Logic 163, 9 (2012) 11631182.

(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) 13811402.

Sharpened Lower Bounds
for Cut Elimination.
Journal of Symbolic Logic 77, 2 (2012) 656668.

(with Arnold Beckmann).
Corrected Upper Bounds
for FreeCut Elimination.
Theoretical Computer Science 412, 39 (2011) 54335445.

(with Alan Johnson).
The Quantifier Complexity of PolynomialSize
Iterated Definitions in FirstOrder Logic.
Mathematical Logic Quarterly, 56, 6 (2010) 573590.

Towards NPP via
Proof Complexity and Search.
Annals of Pure and Applied Logic 163, 7 (2012) 906917.
Also in: Foundational Adventures: Essays in Honor of Harvey Friedman,
Templeton Foundation Press, Article 13, 2012. To appear.

(with Arnold Beckmann).
Characterizing Definable Search Problems
in Bounded Arithmetic via Proof Notations.
In Ways of Proof Theory,
ONTOS Series in Mathematical Logic, pp. 65134, 2010.

(with Daniel Tracy and Bryan Woods).
Efficient LargeScale
Sweep and Prune Methods with AABB Insertion and Removal.
In: IEEE Virtual Reality (VR2009), pp. 191198, 2009.

(with Arnold Beckmann).
Polynomial Local Search in the Polynomial Hierarchy
and Witnessing in Fragments of Bounded Arithmetic.
Journal of Mathematical Logic 9, 1 (2009) 103138.

Pool Resolution is NPhard to Recognize.
Archive for Mathematical Logic 48, 8 (2009) 793798.

(with Roman Kuznets).
Lower
Complexity Bounds in Justification Logic.
Annals of Pure and Applied Logic 163, 7 (2012) 888905.
Earlier conference proceedings version:
The NPCompleteness of
Reflected Fragments of Justification Logics.
In Logical Foundations of Computer Science, LFCS'09,
SpringerVerlag Lecture Notes in Computer Science #5407,
2009, pp. 122136.

(with Jan Hoffmann and Jan Johannsen).
Resolution Trees with Lemmas 
Resolution Refinements that Characterize DLLAlgorithms
with Clause Learning.
Logical Methods in Computer Science, 4, 4:13, 2008.

(with Jan Hoffmann).
The NPhardness of Finding a
Directed Acyclic Graph for Regular Resolution.
Theoretical Computer Science 396 (2008) 271276.

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. 213222.

(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. 20112015.

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. 183208.
Slides from a related talk also available.

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. 153174.
Slides from a related conference presentation also available.

(with Arnold Beckmann).
Separation Results
for the Size of Constantdepth Propositional Proofs.
Annals of Pure and Applied Logic 136, no 12 (2005) 3055.

Collision
Detection with Relative Screw Motion.
The Visual Computer 21 (2005) 4158.

(with JinSu Kim).
Selectively Damped Least
Squares for Inverse Kinematics.
Journal of Graphics Tools, 10, no.3 (2005) 3749.

(with Peter Clote).
Solving the
FisherWright and coalescence problems
with a discrete Markov chain analysis.
Advances in Applied Probability 36, 4 (2004) 117197.

Polynomialsize Frege
and Resolution Proofs of stConnectivity and Hex Tautologies.
Theoretical Computer Science 357, no. 13, (2006) 3552.

(with Nate Segerlind and Russell Impagliazzo).
A Switching Lemma for
Small Restrictions and Lower Bounds for kDNF Resolution.
SIAM Journal on Computing 33, 5 (2004) 11711200.
An earlier version appeared in the
Proceedings of the 43rd Annual Symposium on Foundations of
Computer Science (FOCS'02),
IEEE Computer Society, 2002, pp. 604613.

Accurate
and Efficient Simulations of Rigid Body Rotations.
Journal of Computational Physics 164 (2000) 377406.

(with Alekos Kechris, Anand Pillay and Richard Shore).
Prospects for
Mathematical Logic in the Twentyfirst Century,
Journal of Symbolic Logic 7 (2001) 169196.

(with Bruce Kapron).
Resourcebounded
Continuity and Sequentiality for Typetwo
Functionals,
ACM Transactions on Computational Logic 3 (2002) 402417.
Extended abstract appeared in
Proceedings, 15th IEEE Symposium
on Logic in Computer Science (LICS), 2000, pp. 7783.

(with Arnold Beckmann and Chris Pollett).
Ordinal Notations
and Wellorderings in Bounded Arithmetic,
Annals of Pure and Applied Logic 120 (2002) 197223.
Publisher's erratum:
Annals of Pure and Applied Logic 123 (2003) 291.

(with Pavel Pudlák).
On the Computational
Content of Intuitionistic Propositional Proofs,
Annals of Pure and Applied Logic 109 (2001) 4964.

(with Grigori Rosu).
Incompleteness
of Behavioral Logics,
Proceedings, Coalgebraic Methods in Computer Science, CMCS'2000,
Electronic Notes in Theoretical Computer Science 33 (2000) 6169.

(with Peter Yianilos).
Linear and
O(n log n) Time Minimumcost Matching Algorithms
for Quasiconvex Tours,
SIAM Journal on Computing 27 (1998) 170201.
Expanded version of a paper which appeared in
Proceedings of the Fifth ACMSIAM
Symposium on Discrete Algorithms (SODA), 1994, pp. 6576.
See also associated software and technical report.

(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) 267289.
Earlier version in
Proceedings, 31st Annual ACM Symposium on Theory of Computing
(STOC'99), pp. 547556.
One page abstract in
14th IEEE Conference on Computational Complexity (CCC'99) p. 55.

(with Jay Fillmore).
Spherical Averages
and Applications to Spherical Splines and Interpolation.
ACM Transactions on Graphics 20 (2001) 95126.
Source code for a C++ implementation available too.

(with Grigori Mints).
The
Complexity of the Disjunction and Existence Properties
in Intuitionistic Logic.
Pure and Applied Logic 99 (1999) 93104.

Propositional
Proof Complexity: An Introduction.
In Computational Logic,
edited by U. Berger and H. Schwichtenberg,
SpringerVerlag, Berlin, 1999,
pp. 127178.

An Introduction to Proof
Theory.
In
Handbook of Proof Theory,
edited by S. Buss,
Elsevier NorthHolland, 1998, pp 178.

Firstorder
Proof Theory of Arithmetic.
In
Handbook of Proof Theory,
edited by S. Buss,
Elsevier NorthHolland, 1998, pp 79147.

(with Misha Alekhnovich, Shlomo Moran and Toniann Pitassi).
Minimum Propositional
Proof Length is NPHard to Linearly Approximate.
Journal of Symbolic Logic 66 (2001) 171191.
An extended abstract appeared earlier in
Mathematical Foundations of Computer Science (MFCS'98),
Lecture Notes in Computer Science #1450,
SpringerVerlag, 1998, pp. 176184.

Bounded
Arithmetic, Proof Complexity and Two Papers of Parikh.
Annals of Pure and Applied Logic 96 (1999) 4355.

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,
SpringerVerlag, Berlin, 1997, pp. 1833.

(with Toniann Pitassi).
Resolution
and the Weak Pigeonhole Principle.
In Proceedings, Computer Science Logic (CSL'97),
Lecture Notes in Computer Science #1414,
SpringerVerlag, 1998, pp.149156.

Bounded Arithmetic
and Propositional Proof Complexity.
In Logic of Computation,,
edited by H. Schwichtenberg,
SpringerVerlag, Berlin, 1997, pp. 67122.

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. 5971.

Bounded Arithmetic,
Cryptography and Complexity.
Theoria 63 (1997)147167.

(with Peter Clote).
Cutting Planes,
Connectivity and Threshold Logic.
Archive for Mathematical Logic 35 (1996) 3362.

(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) 256298.

(with Toniann Pitassi).
Good Degree Bounds
on Nullstellensatz Refutations of the Induction Principle.
Journal of Computer and System Sciences 57 (1998) 162171.
Earlier version appeared in Complexity '96, Proceedings of the
Eleventh Annual IEEE Conference on Computational Complexity,
1996, pp 233242.

(with Aleksandar Ignjatović).
Unprovability of Consistency Statements
in Fragments of Bounded Arithmetic.
Annals of Pure and Applied Logic 74 (1995) 221244.

On Herbrand's Theorem.
In Logic and Computational Complexity,
Lecture Notes in Computer Science #960, 1995,
SpringerVerlag, pp. 195209.
 (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,
SpringerVerlag, 1995, pp. 151162.
 (with Maria Luisa Bonet and Toniann Pitassi).
Are There Hard Examples for
Frege Systems?
In Feasible Mathematics II,
Birkhauser, 1995, pp. 3156.

Relating the Bounded Arithmetic and
PolynomialTime Hierarchies.
Annals of Pure and Applied Logic, 75 (1995) 6777.
 (with Maria Luisa Bonet).
SizeDepth Tradeoff
for Boolean Formulae..
Information Processing Letters, 11 (1994) 151155.

Some
Remarks on the Lengths of Propositional Proofs.
Archive for Mathematical Logic 34 (1995) 377394.

On Gödel's Theorems
on Lengths of Proofs I:
Number of Lines and Speedups for Arithmetic.
Journal of Symbolic Logic 39 (1994) 737756.

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. 5790.

(with Maria Luisa Bonet).
On the Serial
Transitive Closure Problem.
SIAM Journal on Computing 24 (1995) 109122.
See also next two items.

(with Maria Luisa Bonet).
The Deduction Rule
and Linear and NearLinear Proof Simulations.
Journal of Symbolic Logic 58 (1993) 688709.
See also previous item and next item.

(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. 286297.
Subsumed by the previous two journal articles.

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 NorthHolland, 1994, pp. 2968.

Algorithms
for Boolean Formula Evaluation and For TreeContraction.
In Proof Theory, Complexity, and Arithmetic,
P. Clote and J. Krajíček (eds),
Oxford University Press, 1993, pp. 95115.

(with Jan Krajíček).
An
Application of Boolean Complexity
to Separation Problems in Bounded Arithmetic.
Proceedings of the London Mathematical Society 69 (1994) 121.

(with Jan Krajíček and Gaisi Takeuti).
Provably Total Functions in the
Bounded Arithmetic Theories
R^{i}_{3}, U^{i}_{2},
and V^{i}_{2}.
In Proof Theory, Arithmetic, and Complexity,
P. Clote and J. Krajíček (eds),
Oxford University Press, 1993, pp. 116161.

The Graph of Multiplication
is Equivalent to Counting.
Information Processing Letters 41 (1992) 199201.

(with Christos Papadimitriou and John Tsitsiklis).
On
the Predictability of Coupled Automata:
an Allegory About Chaos.
Complex Systems 5 (1991) 525539.
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. 788793.

Intuitionistic
Validity in Tnormal Kripke Structures.
Annals of Pure and Applied Logic 59 (1993) 159173.

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. 2747.

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. 142169.

Propositional
Consistency Proofs.
Annals of Pure and Applied Logic 52 (1991) 329.

The Undecidability of kProvability.
Annals of Pure and Applied Logic 53 (1991) 75102.

(with Louise Hay).
On
TruthTable Reducibility to SAT.
Information and Computation 91 (1991) 86102.

(with Louise Hay).
On TruthTable Reducibility to SAT
and the Difference Hierarchy over NP.
In Proceedings of the IEEE Structure in Complexity Conference.
IEEE Computer Society Press, 1988, pp. 224233.

The Modal Logic
of Pure Provability.
Notre Dame Journal of Formal Logic 31 (1990) 225231.

(with Stephen A. Cook and Arvind Gupta and Vijaya Ramachandran).
An Optimal
Parallel Algorithm for Formula Evaluation.
SIAM Journal on Computing 21(1992 755780.

(with Gyorgy Turan).
Resolution
Proofs of Generalized Pigeonhole Principles.
Theoretical Computer Science 62 (1988) 311317.

Axiomatizations
and Conservation Results for Fragments of Bounded Arithmetic.
In Logic and Computation,
Proceedings of a Workshop held at Carnegie Mellon University,
June 30July 2, 1987.
AMS Contemporary Mathematics 106 (1990) 5784.

The
Boolean Formula Value Problem is in ALOGTIME.
In Proceedings of the 19th Annual
ACM Symposium on Theory of Computing (STOC), 1987, pp. 123131.

Polynomial Size Proofs
of the Propositional Pigeonhole Principle.
Journal of Symbolic Logic 52 (1987) 916927.

The
Polynomial Hierarchy and Intuitionistic Bounded Arithmetic.
In Structure in Complexity,
Lecture Notes in Computer Science #223,
Springer Verlag, 1986, pp. 77103.

A Conservation Result
Concerning Bounded Theories and the Collection Axiom.
Proceedings of the American Mathematic Society 100 (1987) 709716.

The
Polynomial Hierarchy and Fragments of Bounded Arithmetic..
In Proceedings of the
17th Annual ACM Symposium on Theory of Computing (STOC'85), 1985,
pp. 285290.

(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. 308313.
Ph.D./Honors theses.

Samuel R. Buss.
Bounded Arithmetic.
Ph.D. thesis,
Department of Mathematics, Princeton University, 1985.
188+v pages.

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.

A review of
Methods of CutElimination
by Matthias Baaz and Alexander Leitsch.
Studia Logica, 103, 3 (2015) 663667.

A review of
Forcing With Random Variables and Proof Complexity
by Jan Krajíček.
Bulletin of Symbolic Logic, 18,4 (2012) 576578.

(with Mia Minnes).
Algorithmic Randomness
with Probabilistic Strategies and Intermediate Success.
Unpublished article. March 2013.

Introduction to Inverse Kinematics
with Jacobian Transpose, Pseudoinverse and Damped Least Squares
methods.
Unpublished survey article, 2004.

(with Rosalie Iemhoff).
The Depth of
Intuitionistic Cut Free Proofs.
Unpublished manuscript 2003.

Studentwritten notes of my
Math 267
 Propositional Proof Complexity course
in Winter 2002.

(with P. Yianilos).
A Bipartite Matching
Approach to Approximate String Comparison and Search.
Unpublished manuscript.

(with P. Yianilos).
Secure ShortKey
Cryptosystems: Forty Bits is Enough.
Unpublished manuscript.

Lectures
on Proof Theory
Technical Report number SOCS96.1,
School of Computer Science, McGill University, 1996,
117 pages.

A review
of the biography of K. Godel,
Logical Dilemmas,
by John Dawson.
SIAM Review 40 (1998) 397400.

Studentwritten notes of my
Math 267 
Mathematical Foundations of Cryptography course
in Winter 1997.

(with Peter Clote).
Threshold logic proof systems.
Unpublished manuscript.
May 1995.

(with D. Robinson, K. Kanzelberg, P. Yianilos).
Solving
the MinimumCost Matching Principle for QuasiConvex 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.

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) 261261.
Reprinted in SIGACT News 24 (1993) 4141.

Studentwritten notes of my
Math 267 
Circuit Complexity course
in WinterSpring 1992.

A review of three papers of Neil Immerman,
Journal of Symbolic Logic 54 (1989) 287288.

(with S.A. Cook, P.W. Dymond and L. Hay).
The
log space oracle hierarchy collapses.
Technical report #CS87103.
Computer Science Engineering Department,
Univ. of California, San Diego, 1987.

Studentwritten notes for Math 260AC on
Introduction
to Mathematical Logic.
Fall 1988Spring 1989.

Studentwritten notes of my Math 271 (Berkeley) topics course on
Weak Formal Systems
and Connections to Computational Complexity,
WinterSpring 1988.

Neighborhood Metrics
on nDimension Blocks of Characters,
Technical report #0021886,
Mathematical Sciences Research Institute,
Berkeley, California,
September 1985.
Selected talks.

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.

Some Challenge Problems
for Resolution and One Also for AC^{0}Frege
or:Seeking Hard Instances for Constant Depth Frege.
Art of SAT, Shonan, Village, Japan,
October 2, 2023.

DRAT Proofs and Extensions:
Satisfiability Solving with Conflict Driven Clause Learning
and Nonimplicational Inferences
`University of Birmingham, June 15, 2023.

On Extended Frege Proofs.
ToniCS,
Simons Institute, Berkeley,
March 28, 2023.

Gödel and Lengths of Proofs.
Celebrating 90 Years of Gödel's Incompleteness Theorems,
University of Tübingen,
July 8, 2021.

CDCL Solvers, Resolution,
Extension and DRAT Proofs.
Orevkov'80, 5th St. Peterburg Days in Logic and Computability,
May 15, 2021.

Proof Complexity Boot Camp.
Slides for four prerecorded videos and one live zoom presentation.
Special Program in Satisfiability, Simons Institute,
February 3, 2021.

Propositional Branching Program Proofs
and Logics for L and NL.
Logic Seminar, Czech Academy of Sciences,
Prague, November 14, 2020.

Proof Complexity and Bounded Arithmetic.
Four lectures,
Caleidoscope Research School in Computational Complexity,
Institut Henri Poincare,
Paris, June 1718, 2019.

Totality, Provability, and
Feasibility.
Gödel Lecture,
ASL Annual Meeting,
CUNY, New York,
May 22, 2019

Bounded Arithmetic, Expanders and
Monotone Propositional Proofs.
Takeuti Symposium on Advances in Logic,
Kobe, Japan,
September 20, 2018.

Introduction to
Bounded Arithmetic,
Workshop on Proof Complexity,
St. Petersburg State University,
May 15, 2016.

Nonconstructive Proofs of
Existence for Provably Total Search Problems.
Presentation at Workshop on Theoretical Computer Science,
Higher School of Economics,
Moscow, April 2016.

Nelson's Formalist
Approach to Feasible Arithmetic
and the Foundations of Mathematics.
Presentation at American Philosophical Association, Western Division
Meeting,
San Francisco,
March 2016.

Provably Total Search Problems
of SecondOrder Bounded Arithmetic.
Existence for Provably Total Search Problems
Journes sur les Arithmetiques Faibles (JAF) and MAMLS,
New York City, July 2015.

On the Power of Diagonalization for
Separating Complexity Classes,
Yandex, Moscow, Russia,
July 2015.

Tutorial on Proof Systems Related
to SAT Solvers,
Workshop on Theory and Practice of SAT Solving,
Dagstuhl, Germany, April 2015.

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.

Complexity
of Propositional Proofs: Some Theory and Examples
UPC, Barcelona, April 2015
and Swansea University, March 2015.

Search Problems, Proof Complexity,
and SecondOrder Bounded Arithmetic.
Logic and Computational Complexity, Summer of Logic, Vienna.
July 2014.

Towards (Non)Separations
in Propositional Proof Complexity.
Stanford University,
February 2014.

MiniTutorial on Proof Complexity.
Workshop on Theoretical Foundations of SAT Solving.
BIRS, Banff, Canada.
January 2014.

Collapsing Modular Counting
in Bounded Arithmetic and Constant Depth Propositional Proofs.
Limits of Theorem Proving (LiThPr).
Rome, Italy,
September 2012.

An Improved Separation
of Regular Resolution
from Pool Resolution and Clause Learning.
Theory and Applications of Satisfiability Testing (SAT 2012).
Trento, Italy,
June 2012.

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.

Expressibility,
and the Complexity of Proofs,
PhilMath Intersem, Paris 7 Diderot,
June 2011.

Proof Complexity and the
Complexity of SAT Solvers,
First International SAT/SMT Solver Workshop,
Boston, June 2011.

Limits on AlternationTrading Proofs
for TimeSpace Bounds for Satisfiability,
Barcelona, February 2011; Wales, March 2011; Paris, June 2011.

SAT Solver Trials:
Experiments with a SAT Solver,
Infinity Project,
Centre de Recerca Matemàtica, Barcelona, Spain,
December 2009.

A series of four talks on
NP Functions, Local Search, and Bounded Arithmetic,
Prague Fall School on Logic and Complexity,
September 2009.

Towards NPP and Satisfiability
via Proof Complexity and Proof Search,
Logical Foundations of Computer Science (LFCS'09),
January 2009.

The NPCompleteness
of Reflected Fragments of Justification Logics,
Logical Foundations of Computer Science (LFCS'09), January 2009.

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.

Large Numbers,
Busy Beavers, Noncomputability and Incompleteness,
Food for Thought seminar,
UCSD, November 2007.

The Computational Power
of Bounded Arithmetic from the Predicative Viewpoint,
ASL Winter Meeting, special session,
January 2007.

Propositional
Proof Systems and Search,
Connections II: Fundamentals of Network Science,
Caltech,
August 2006.

Proof Complexity
and Computational Hardness,
Computability in Europe (CiE),
July 2006, Swansea, Wales.
Three tutorial lectures.

Bounded Arithmetic,
ConstantDepth Proofs and stConnectivity.
UCLA Logic Meeting (VIG),
February 2004.
Contains stConnectivity and Hex tautology work.

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.

Is It Easier To "Discover"
Than To "Verify"?.
UCSD Math Circle presentation to high school students.
May 22, 2004.

Bounded Arithmetic
and Bounded Depth Propositional Proofs.
Takeuti Symposium on Mathematical Logic.
Kobe, Japan, December, 2003.

Polynomialsize Frege
and Resolution Proofs of stConnectivity and Hex Tautologies
Workshop on Proof Theory, Muenster, October 2003;
and 12th Latin American Symposium on Mathematical Logic (SLALM),
Costa Rica, January 2004.

Spherical Splines
and Applications to Spherical Splines and Interpolation.
Pixel Cafe, UCSD, December 2002.

Taylor series methods
for rigid body simulation and extensions to Lie groups.
Seventh SIAM Conference on Geometric Design and Computing.
Sacramento.
November 2001.

Bounded arithmetic
and propositional proofs.
NATO International Summer School on Logic of Computation.
Marktoberdorf, Germany.
JulyAugust 1995.
Five hours of lectures.
Selected Ph.D. dissertations by students.
(More can be available upon request.)

David Robinson,
Parallel
Algorithms for Group Word Problems,
Ph.D. Thesis, Department of Mathematics,
University of Califoria, San Diego, 1993.

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

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.

Samuel R. Buss and Peter N. Yianilos,
Linear and Nonlinear 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.)
 Grand Theft Auto: Episodes from Liberty City., Rockstar Games, 2010.
 Grand Theft Auto IV: The Lost and Damned., Rockstar Games, 2010.
 Grand Theft Auto: The Ballad of Gay Tony., Rockstar Games, 2010.
 Grand Theft Auto IV, Rockstar Games, 2008.
 Smuggler's Run: Warzones, Rockstar Games, 2002.
 TransWorld SURF, Infogames, 2002.
 Smuggler's Run 2: Hostile Territory, Rockstar Games, 2001.
 Midnight Club: Street Racing, Rockstar Games, 2000.
 Midtown Madness 2, Microsoft Game Studios, 2000.
 Smuggler's Run, Rockstar Games, 2000.
 Midtown Madness, Microsoft Game Studios, 1999.