Some Presentations
On this webpage you find a generous selection of slides (and
sometimes video recordings) for presentations that I have given.
Everything should be sorted (at least roughly) in reverse
chronological order.
Links go bad from time to time. If you discover anything that is
broken, I would be most grateful if you would
drop me a line.

Tutorials on
SAT Solving
,
PseudoBoolean Solving
,
PseudoBoolean Optimization
,
and
Mixed Integer Linear Programming and PseudoBoolean Solving/Optimization
given at the
1st International Workshop on
Solving Linear Optimization Problems for PseudoBooleans and Yonder
(SLOPPY '24)
in Lund, Sweden,
November 2024.
(Also available as video recordings of
part 1,
part 2,
part 3,
and
part 4.)

Supercritical and Robust Tradeoffs for Resolution Depth Versus Width
and Weisfeiler–Leman.
Talk given at the Dagstuhl seminar
SAT and Interactions,
October 2024.

Sure, Your Algorithm Is Really Fast, But Is It Really Correct?
Talk in the
DIKU Bits
series at the University of Copenhagen, September 2024.

Certified MaxSAT Preprocessing.
Talk given at the
Pragmatics of SAT
workshop in Pune, India, August 2024.

EndtoEnd Verification for Subgraph Solving.
Talk given at the
Pragmatics of SAT
workshop in Pune, India, August 2024.

Combinatorial Solving with Provably Correct Results.
Talk given at the
25th International Symposium on Mathematical Programming
in Montréal, Canada, July 2024.

Proof Complexity and SAT Solving.
Lecture given at the
SAT/SMT/AR Summer School
in Nancy, France,
June 2024.

A OneSizeFitsAll Proof Logging System?
Talk given at the
1st International Workshop on Highlights in Organizing and Optimizing Prooflogging Systems
(WHOOPS '24)
in Copenhagen, Denmark, May 2024.

Certifying Combinatorial Solving Using
Cutting Planes with Strengthening Rules
Talk given at the Oberwolfach workshop
Proof Complexity and Beyond,
March 2024.

Complexity Theory for RealWorld Computation.
Talk given at the workshop
Complexity Days
in Paris, France,
December 2023.

A Unified Proof System for Discrete Combinatorial Problems.
Talk given at the Dagstuhl seminar
The Next Generation of Deduction Systems:
From Composition to Compositionality,
November 2023.

A OneSizeFitsAll Proof Logging System?
Talk given at the
Pragmatics of SAT
workshop in Alghero, Italy, July 2023,
and (slightly revised) at the
NII Shonan Meeting 180 "The Art of SAT",
October 2023.

Certified CNF Translations for PseudoBoolean Solving.
Brief talk given
in the Best Papers from Sister Conferences Track at
IJCAI '23
in Macau, China, August 2023.

Combinatorial Solving with Provably Correct Results.
Tutorial (joint with Bart Bogaerts and Ciaran McCreesh) given at
IJCAI '23
in Macau, China, August 2023.

Certified Symmetry and Dominance Breaking for Combinatorial Optimisation.
Brief talk given at the Dagstuhl seminar
SAT Encodings and Beyond,
June 2023.

Leveraging Computational Complexity Theory
for Provably Correct Combinatorial Optimization.
Talk given at the
North American Annual Meeting
of the Association for Symbolic Logic,
at UC Irvine,
March 2023.

Certifying Combinatorial Solving Using
Cutting Planes with Strengthening Rules.
Talk given at the
Proof Complexity and MetaMathematics workshop
at the Simons Institute for the Theory of Computing at UC Berkeley,
March 2023.
(Also available in
video.)

The Computational Challenge of Combinations.
Inaugural professorial lecture given at
Lund University and
the University of Copenhagen,
February 2023.

Lectures on
SAT Solving
,
PseudoBoolean Solving
,
PseudoBoolean Optimization
,
and
Mixed Integer Linear Programming and PseudoBoolean Solving/Optimization
at the
Indian SAT+SMT Winter School
in Chennai, India,
December 2022.
(Also available as video recordings of
part 1,
part 2,
part 3,
part 4,
and
demo session.)

Combinatorial Solving with Provably Correct Results.
Tutorial (joint with Bart Bogaerts and Ciaran McCreesh) given
in the
MIAO seminar series,
November 2022.
(Also available in
video.)

Certified CNF Translations for PseudoBoolean Solving.
Brief talk given at the
Swedish Operations Research Conference (SOAK 2022)
in Stockholm, Sweden, October 2022.

Certified Symmetry and Dominance Breaking for Combinatorial Optimisation.
Brief talk given at the
Swedish Operations Research Conference (SOAK 2022)
in Stockholm, Sweden, October 2022.

Proof Complexity and SAT Solving.
Survey talk given at the Dagstuhl seminar
Theory and Practice of SAT and Combinatorial Solving,
October 2022.

Solving with Provably Correct Results:
Beyond Satisfiability, and Towards Constraint Programming.
Tutorial (joint with Bart Bogaerts and Ciaran McCreesh) given at
CP '22
in Haifa, Israel, August 2022.

Certified Symmetry and Dominance Breaking for Combinatorial Optimisation.
Brief talk given at the
Pragmatics of SAT
workshop in Haifa, Israel, August 2022.

Adding Dual Variables to Algebraic Reasoning for GateLevel Multiplier Verification.
Brief talk given at the
Pragmatics of SAT
workshop in Haifa, Israel, August 2022.

Proof Logging for Combinatorial Optimization
Using PseudoBoolean Reasoning.
Survey talk given at the reunion workshop for the
Satisfiability: Theory, Practice, and Beyond
semester program at the
Simons Institute for the Theory of Computing at UC Berkeley,
June 2022.

Lectures on
Boolean Satisfiability (SAT) Solving
and
PseudoBoolean Solving
given in the
Logics in Computer Science
course at the
University of Copenhagen,
January 2022.

Leveraging Computational Complexity Theory for
Verifiably Correct Combinatorial Optimization.
Brief talk given at the
Digital Research Centre Denmark (DIREC) Workshop
in Nyborg, Denmark,
September 2021.

Proofs, Proof Logging, Trust, and Certification.
Brief talk given at the Dagstuhl seminar
Extending the Synergies Between SAT and Description Logics,
September 2021.

PseudoBoolean Solving: In Between SAT and ILP
Brief talk given at the
Theoretical Foundations of SAT/SMT Solving
workshop/seminar series at the
Simons Institute for the Theory of Computing at UC Berkeley,
March 2021.
(Also available in
video.)

PseudoBoolean Solving and Optimization.
Tutorial given at the boot camp workshop for the
Satisfiability: Theory, Practice, and Beyond
program at the
Simons Institute for the Theory of Computing at UC Berkeley,
February 2021.
Slides for live talk
(with
video)
and slides for the longer version
(with prerecorded videos of
part I,
part II,
part III,
and
part IV
of the tutorial).

Subgraph Isomorphism Meets Cutting Planes:
Towards Verifiably Correct Constraint Programming.
Talk given at KU Leuven, September 2019,
and at the University of Copenhagen, January 2020.

Nullstellensatz SizeDegree Tradeoffs from Reversible Pebbling.
Brief talk given at the Algorithms and Complexity Section
at the University of Copenhagen,
December 2019.

On Division Versus Saturation in Cutting Planes.
Talk given at the reunion workshop for the
Lower Bounds in Computational Complexity
semester program at the
Simons Institute for the Theory of Computing at UC Berkeley,
December 2019.

Learn to Relax: Integrating Integer Linear Programming
with ConflictDriven Search.
Talk given at Imperial College London, December 2019.

Solving Exponentially Hard Problems in Linear Time(?).
Talk in the
DIKU Bits
series at the University of Copenhagen, December 2019

Subgraph Isomorphism Meets Cutting Planes.
Talk given at the
NordConsNet 2019 workshop,
May 2019.

Using PseudoWidth to Prove Lower Bounds
for Highly Overconstrained Formulas.
Talk given at the Dagstuhl seminar
Computational Complexity of Discrete Problems,
March 2019.

On Division Versus Saturation in Cutting Planes.
Talk given at the Dagstuhl seminar
Bringing CP, SAT and SMT together:
Next Challenges in Constraint Solving,
February 2019.

Proof Complexity Lower Bounds from Graph Expansion and Combinatorial Games.
Talk given at the
Algebraic Methods workshop at the
Simons Institute for the Theory of Computing at UC Berkeley,
December 2018.
(Also available in
video.)

NearOptimal Lower Bounds on Quantifier Depth and
Weisfeiler–Leman Refinement Steps.
Talk given at the University of Copenhagen,
September 2018.

Divide and Conquer:
Towards Faster ConflictDriven PseudoBoolean Solving.
Talk given at the University of Copenhagen,
September 2018.

Towards Faster ConflictDriven PseudoBoolean Solving.
Survey talk given at the workshop
Theory and Practice of Satisfiability Solving
at Casa Matemática Oaxaca,
August 2018.
(Also available in
video.)

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks.
Brief talk given at
IJCAIECAI '18
in Stockholm, Sweden, July 2018.

Reasoning in Propositional Logic Using Gröbner Bases.
Talk given at
Lund University,
May 2018.
Handwritten
notes

Beyond Satisfaction:
Towards an Understanding of RealWorld Efficient Computation
Brief talk given at the SRA ICT TNG Research Challenge Day at KTH,
May 2018.

Solving Logic Formulas in Linear Time (At Least Surprisingly Often)
Brief talk given at the University of Copenhagen,
April 2018.

Supercritical SpaceWidth Tradeoffs for Resolution.
Talk given at the Dagstuhl seminar
Proof Complexity,
JanuaryFebruary 2018.

Lower Bound Techniques for Nullstellensatz and Polynomial Calculus.
Survey talk given at the Dagstuhl seminar
Proof Complexity,
JanuaryFebruary 2018.
Handwritten
notes

Understanding ConflictDriven SAT Solving Through the
Lens of Proof Complexity.
Talk given at
Lund University,
November 2017,
and in the KTH Theory reading group,
November 2017.

Proof Complexity Lower Bounds from Graph Expansion and Combinatorial Games.
Talk given at
IT University of Copenhagen, October 2017.

Using Combinatorial Benchmarks to Probe the
Reasoning Power of PseudoBoolean Solvers.
Brief talk given at the
Pragmatics of Constraint Reasoning
workshop in Melbourne, Australia, August 2017.

A Generalized Method for Resolution and Polynomial Calculus Lower Bounds.
Talk given at the Dagstuhl seminar
Computational Complexity of Discrete Problems,
March 2017.

Understanding ConflictDriven SAT Solving
Through the Lens of Proof Complexity.
Survey talk given at the workshop
Theoretical Foundations of SAT Solving
at the Fields Institute in Toronto, Canada,
August 2016,
and at IIT Bombay in Mumbai, India, February 2017.

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds.
Talk given at the workshop on proof complexity during the
Special Semester Program on Complexity Theory
in St. Petersburg, Russia, May 2016,
and at the Tata Institute of Fundamental Research, Mumbai, India,
February 2017.

Supercritical SpaceWidth Tradeoffs for Resolution.
Talk given at the Dagstuhl seminar
SAT and Interactions,
September 2016,
and at Rutgers University, New Jersey, USA,
October 2016.

Tradeoffs Between Time and Memory in a
Tighter Model of CDCL SAT Solvers.
Brief talk given at
SAT '16
in Bordeaux, France, July 2016.

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks.
Brief talk given at the
7th Pragmatics of SAT
workshop in Bordeaux, France, July 2016.

On the Interplay Between Proof Complexity and SAT Solving.
Tutorialstyle talk
given at the
International Summer School on Satisfiability, Satisfiability
Modulo Theories, and Automated Reasoning
in Lisbon, Portugal, June 2016.

How Limited Interaction Hinders Real Communication
(and What It Means for Proof and Circuit Complexity).
Brief talk given at the
CCC 2016 Satellite Kyoto Workshop
in Kyoto, Japan, June 2016.

How Limited Interaction Hinders Real Communication
(and What It Means for Proof and Circuit Complexity).
Talk given at the
Workshop on Algorithms in Communication Complexity, Property Testing
and Combinatorics
at the Skolkovo Institute of Science and Technology,
in Moscow, Russia, April 2016.

On the Interplay Between Proof Complexity and SAT Solving.
Long survey talk given at the
National Research University Higher School of Economics
in Moscow, Russia, April 2016.
(Also available in
video.)

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds.
Talk given at the program
Semidefinite and Matrix Methods for Optimization and Communication
at the Institute for Mathematical Sciences in Singapore, February 2016.

A Survey of Proof Complexity from a SAT Solving Perspective.
Talk given at Uppsala University, November 2015.

I skärningspunkten mellan beviskomplexitet och SATlösning.
Docent (habilitation) lecture given at
KTH Royal Institute of Technology, November 2015.

A (Biased) Proof Complexity Survey for SAT Practitioners.
Talk given at Université d'Artois in Lens, France,
February 2015.

Exploring Connections Between Proof Complexity
and Practical Hardness of SAT.
Talk given at Université d'Artois in Lens, France,
February 2015.

TimeSpace Tradeoffs in Proof Complexity (and SAT Solving?).
Talk given at the workshop
Algorithms, Complexity and Machine Learning:
A Tribute to Kurt Mehlhorn
at Chalmers University of Technology, Göteborg, October 2014.

A (Biased) Proof Complexity Survey for SAT Practitioners.
Invited talk given at SAT '14
in Vienna, Austria, July 2014.

A (Biased) Survey of Space Complexity and
TimeSpace Tradeoffs in Proof Complexity.
Invited talk given at the proof complexity workshop at
FLoC '14
in Vienna, Austria, July 2014.

Narrow Proofs May Be Maximally Long.
Talk given at the University of Chicago, May 2014.

MiniTutorial on Weak Proof Systems and Connections to SAT Solving.
Talk given at the workshop
Theoretical Foundations of Applied SAT Solving
at the Banff International Research Station in Canada, January 2014.
(Also available in
video.)

Relating Proof Complexity Measures and Practical Hardness of SAT.
Talk given at the
First Symposium on Structure in Hard Combinatorial Problems
in Vienna, Austria, May 2013.

Rediscovering the Joys of Pebbling.
Talk given in the KTH Theory reading group,
April 2013.

Relating Proof Complexity Measures and Practical Hardness of SAT.
Talk given at the Dagstuhl seminar
SAT Interactions,
November 2012,
and at the University of Toronto, January 2013.

Relating Proof Complexity Measures and Practical Hardness of SAT.
Brief overview talk given at
CP '12, October 2012.

On the Virtue of Succinct Proofs:
Amplifying Communication Complexity Hardness to
TimeSpace Tradeoffs in Proof Complexity.
Talk given at the
Limits of Theorem Proving workshop in Rome, Italy, September 2012,
and (slightly revised) in the KTH Theory reading group, October 2012,
and at the Tata Institute of Fundamental Research in Mumbai, India, March 2013.

On the Virtue of Succinct Proofs:
Amplifying Communication Complexity Hardness to
TimeSpace Tradeoffs in Proof Complexity.
Brief overview talk given at
STOC '12, May 2012.

Understanding the Hardness of Proving Formulas in Propositional Logic.
Updated version of a
survey talk about SAT solving, proof complexity, and timespace tradeoffs in resolution and other proof systems
given at Stockholm University,
November 2011.

On Minimal Unsatisfiability and TimeSpace Tradeoffs for kDNF Resolution.
Brief talk given at
ICALP '11,
July 2011.

On Proof Complexity Lower Bounds and Possible Connections to SAT Solving.
Brief talk given at the
Synergies in Lower Bounds
workshop at Aarhus University, Denmark,
JuneJuly 2011,
and (slightly revised)
at the Oberwolfach workshop
Mathematical Logic: Proof Theory, Constructive Mathematics,
November 2011.

On the Semantics of Local Characterizations
for LinearInvariant Properties.
Brief talk given at the Dagstuhl seminar on
Computational Complexity of Discrete Problems,
March 2011.

On the Semantics of Local Characterizations
for LinearInvariant Properties.
Talk given
in the KTH Theory Group seminar series, November 2010,
and (slightly revised) at the
Technion – Israel Institute of Technology in Haifa, Israel,
December 2010.

Understanding the Hardness of Proving Formulas in Propositional Logic.
Survey talk about SAT solving, proof complexity, and resolution timespace tradeoffs
given at Lund University,
October 2010
and in a slightly expanded and more technical version at the
Complexity and Finite Models (CMF 2011) workshop
in Paris, June 2011.

Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions.
Brief overview talk, with a slightly more applied angle, given at the
Propositional Proof Complexity: Theory and Practice workshop at
FLoC '10,
July 2010,
and (in a slightly shorter version) at
ICS '11,
January 2011.

Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions.
Yet another survey talk
about my PhD thesis and some subsequent work,
but with a slightly more applied angle, given at the
International Workshop on Tractability
at Microsoft Research Cambridge, UK, July 2010.

On the Relative Strength of Pebbling and Resolution.
Brief overview talk given at
CCC '10,
June 2010,
and in the KTH Theory Group seminar series, October 2010.

Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions.
Survey talk about my PhD thesis and some subsequent work given
in the CSAIL Theory of Computation Colloquium series,
April 2010 and then (slightly revised) at the University of Toronto and
at KTH, May 2010.
Yet another modified and updated version of this talk, but with the title
Understanding the Hardness of Proving Formulas in Propositional Logic,
was given at the proof complexity workshop
at the Banff International Research Station in Canada, October 2011.

Understanding Space in Proof Complexity.
Survey talk about my PhD thesis and some subsequent work given
at the Ackermann Award ceremony at
CSL '09,
September 2009.

Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions.
Brief overwiev talk
about the ECCC reports
TR09034
and
TR09047
given at the Barriers in Computational Complexity workshop in Princeton, USA, August 2009.

Guest lectures about proof complexity
on the
Advanced Complexity Theory
course
at MIT,
April 2009.
Handwritten
lecture notes
and (mostly accurate)
scribed notes for lecture 1
and
lecture 2.

Understanding Space in Resolution: Optimal Lower Bounds and Exponential Tradeoffs.
Talkabout our
FOCS '08 paper
and
ECCC report TR09034
given at the Dagstuhl seminar on
Computational Complexity of Discrete Problems,
September 2008,
and (slightly revised) in the MIT CSAIL Algorithms and Complexity Seminar series, October 2008.

Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.
Brief overview talk given at
FOCS '08,
October 2008.

Towards an Optimal Separation of Space and Length in Resolution.
Brief overview talk given at
STOC '08
and at the NORDITA
Physics of distributed information systems (PhysDIS)
workshop in Stockholm, May 2008.

Towards an Optimal Separation of Space and Length in Resolution.
Talk given at
the Technion – Israel Institute of Technology in Haifa
and
the Weizmann Institute of Science in Rehovot,
Israel, March 2008.
Some technical slides in the appendix.

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution.
Very detailed technical talk in the KTH Theory Group seminar series, June 2006.

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution.
Brief overview talk given at
STOC '06,
May 2006.

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution.
Somewhat detailed talk given at
the Dagstuhl seminar on
Complexity of Boolean Functions in March 2006
and (slightly revised) at the Isaac Newton Institute Workshop
New Directions in Proof Complexity in Cambridge, UK, in April 2006.

Short Proofs Are Narrow (Well, Sort of), But Are They Tight?
Fairly technical talk about width and space in resolution
in the KTH Theory Group PhD student seminar series, April 2006.

Stålmarck's Method versus Resolution: A Comparative Theoretical Study.
Rather informal overview of the subject matter of my Master's thesis, November 2001.

Stålmarck's Method versus Resolution: A Comparative Theoretical Study.
More technical account of the most important results in my Master's thesis, November 2001.
