Daniela Kaufmann, Paul Beame, Armin Biere and Jakob Nordström.
Adding Dual Variables to Algebraic Reasoning for Circuit Verification.
To appear in
Proceedings of the 25th
Design, Automation and Test in Europe Conference (DATE '22),
March 2022.
Susanna F. de Rezende, Massimo Lauria, Jakob Nordström,
and Dmitry Sokolov.
The Power of Negative Reasoning.
In
Proceedings of the 36th Annual Computational Complexity Conference (CCC '21),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 200, pages 40:1-40:24,
July 2021.
Susanna F. de Rezende, Mika Göös, Jakob Nordström,
Toniann Pitassi, Robert Robere, and Dmitry Sokolov.
Automating Algebraic Proof Systems is NP-Hard.
In
Proceedings of the 53rd Annual ACM Symposium on Theory of Computing
(STOC '21),
pages 209-222,
June 2021.
Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
To appear in
Journal of the ACM, 2021.
Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria,
Jakob Nordström, and Alexander Razborov.
Clique Is Hard on Average for Regular Resolution.
In
Journal of the ACM,
volume 68, issue 4, pages 23:1-23:26,
August 2021.
Jo Devriendt, Stephan Gocht, Emir Demirović,
Jakob Nordström, and Peter Stuckey.
Cutting to the Core of Pseudo-Boolean Optimization:
Combining Core-Guided Search with Cutting Planes Reasoning.
In
Proceedings of the
35th AAAI Conference on Artificial Intelligence (AAAI '21),
pages 3750-3758,
February 2021.
Stephan Gocht and Jakob Nordström.
Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs.
In
Proceedings of the
35th AAAI Conference on Artificial Intelligence (AAAI '21),
pages 3768-3777,
February 2021.
Susanna F. de Rezende, Or Meir, Jakob Nordström, and Robert Robere.
Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling.
Computational Complexity,
February 2021.
Jo Devriendt, Ambros Gleixner, and Jakob Nordström.
Learn to Relax: Integrating 0-1 Integer Linear Programming
with Conflict-Driven Pseudo-Boolean Search.
Constraints,
January 2021.
(Special issue for CPAIOR '20.)
Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals.
How Limited Interaction Hinders Real Communication
(and What It Means for Proof and Circuit Complexity).
Technical Report TR21-006,
Electronic Colloquium on Computational Complexity (ECCC),
January 2021.
Susanna F. de Rezende, Or Meir, Jakob Nordström,
Toniann Pitassi, Robert Robere, and Marc Vinyals.
Lifting with Simple Gadgets and Applications to
Circuit and Proof Complexity.
In
Proceedings of the 61st Annual IEEE Symposium on
Foundations of Computer Science (FOCS '20),
pages 24-30, November 2020.
Susanna F. de Rezende, Or Meir, Jakob Nordström,
Toniann Pitassi, and Robert Robere.
KRW Composition Theorems via Lifting.
In
Proceedings of the 61st Annual IEEE Symposium on
Foundations of Computer Science (FOCS '20),
pages 43-49, November 2020.
Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, and Jakob Nordström.
Verifying Properties of Bit-vector Multiplication
Using Cutting Planes Reasoning.
In
Proceedings of the 20th Conference on
Formal Methods in Computer-Aided Design (FMCAD '20),
pages 194-204, September 2020.
Jo Devriendt, Ambros Gleixner, and Jakob Nordström.
Learn to Relax: Integrating 0-1 Integer Linear Programming
with Conflict-Driven Pseudo-Boolean Search.
In
Proceedings of the 17th International Conference on the
Integration of Constraint Programming, Artificial Intelligence,
and Operations Research (CPAIOR '20),
pages xxiv-xxv, September 2020.
Stephan Gocht, Ciaran McCreesh and Jakob Nordström.
VeriPB: The Easy Way to Make Your
Combinatorial Search Algorithm Trustworthy.
From Constraint Programming to Trustworthy AI,
workshop at the
26th International Conference
on Principles and Practice of Constraint Programming (CP '20),
September 2020.
(See also the
video
from the workshop.)
Stephan Gocht, Ross McBride, Ciaran McCreesh,
Jakob Nordström, Patrick Prosser, and James Trimble.
Certifying Solvers for Clique and Maximum
Common (Connected) Subgraph Problems.
In
Proceedings of the 26th International Conference on
Principles and Practice of Constraint Programming (CP '20),
Lecture Notes in Computer Science, volume 12333,
pages 338-357, September 2020.
Janne I. Kokkala and Jakob Nordström.
Using Resolution Proofs to Analyse CDCL Solvers.
In
Proceedings of the 26th International Conference on
Principles and Practice of Constraint Programming (CP '20),
Lecture Notes in Computer Science, volume 12333,
pages 427-444, September 2020.
Buser Say, Jo Devriendt, Jakob Nordström, and Peter Stuckey.
Theoretical and Experimental Results for Planning with Learned
Binarized Neural Network Transition Models.
In
Proceedings of the 26th International Conference on
Principles and Practice of Constraint Programming (CP '20),
Lecture Notes in Computer Science, volume 12333,
pages 917-934, September 2020.
Susanna F. de Rezende, Jakob Nordström,
Kilian Risse, and Dmitry Sokolov.
Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and
Perfect Matching Formulas over Sparse Graphs.
In
Proceedings of the 35th Annual Computational Complexity Conference (CCC '20),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 169, pages 28:1-28:24,
July 2020.
Susanna F. de Rezende, Or Meir, Jakob Nordström,
Toniann Pitassi, and Robert Robere.
KRW Composition Theorems via Lifting.
Technical Report TR20-099,
Electronic Colloquium on Computational Complexity (ECCC),
July 2020.
Marc Vinyals, Jan Elffers, Jan Johannsen, and Jakob Nordström.
Simplified and Improved Separations Between Regular and General Resolution by Lifting.
In
Proceedings of the 23rd International Conference on
Theory and Applications of Satisfiability Testing (SAT '20),
Lecture Notes in Computer Science, volume 12178,
pages 182-200, July 2020.
Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
Subgraph Isomorphism Meets Cutting Planes:
Solving with Certified Solutions.
In
Proceedings of the 29th International Joint Conference on
Artificial Intelligence (IJCAI '20),
pages 1134-1140,
July 2020.
Susanna F. de Rezende, Mika Göös, Jakob Nordström,
Toniann Pitassi, Robert Robere, and Dmitry Sokolov.
Automating Algebraic Proof Systems is NP-Hard.
Technical Report TR20-064,
Electronic Colloquium on Computational Complexity (ECCC),
May 2020.
Christoph Berkholz and Jakob Nordström.
Supercritical Space-Width Trade-offs for Resolution.SIAM Journal on Computing,
volume 49, issue 1, pages 98-118, February 2020.
Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
Justifying All Differences Using Pseudo-Boolean Reasoning.
In
Proceedings of the
34th AAAI Conference on Artificial Intelligence (AAAI '20),
pages 1486-1494,
February 2020.
Jan Elffers and Jakob Nordström.
A Cardinal Improvement to Pseudo-Boolean Solving.
In
Proceedings of the
34th AAAI Conference on Artificial Intelligence (AAAI '20),
pages 1495-1503,
February 2020.
Guillaume Lagarde, Jakob Nordström, Dmitry Sokolov, and Joseph Swernofsky.
Trade-offs Between Size and Degree in Polynomial Calculus.
In
Proceedings of the 11th Innovations in
Theoretical Computer Science Conference (ITCS '20),
pages 72:1-72:16,
January 2020.
Susanna F. de Rezende, Or Meir, Jakob Nordström,
Toniann Pitassi, Robert Robere, and Marc Vinyals.
Lifting with Simple Gadgets and Applications to
Circuit and Proof Complexity.
Technical Report 2001.02144,
arXiv.org,
January 2020.
Susanna F. de Rezende, Jakob Nordström,
Kilian Risse, and Dmitry Sokolov.
Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and
Perfect Matching Formulas over Sparse Graphs.
Technical Report TR19-174,
Electronic Colloquium on Computational Complexity (ECCC),
December 2019.
Stephan Gocht, Jakob Nordström, and Amir Yehudayoff.
On Division Versus Saturation in Pseudo-Boolean Solving.
In
Proceedings of the 28th International Joint Conference on
Artificial Intelligence (IJCAI '19),
pages 1711-1718,
August 2019.
Susanna F. de Rezende,
Jakob Nordström,
Or Meir,
and Robert Robere.
Nullstellensatz Size-Degree Trade-offs from
Reversible Pebbling.
In
Proceedings of the 34th Annual Computational Complexity Conference (CCC '19),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 137, pages 18:1-18:26,
July 2019.
Jan Elffers and Jakob Nordström.
Divide and Conquer: Towards Faster Pseudo-Boolean Solving.
In
Proceedings of the 27th International Joint Conference on
Artificial Intelligence (IJCAI '18),
pages 1291-1299, July 2018.
Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, Jakob Nordström, and
Laurent Simon.
Seeking Practical CDCL Insights from Theoretical SAT Benchmarks.
In
Proceedings of the 27th International Joint Conference on
Artificial Intelligence (IJCAI '18),
pages 1300-1308, July 2018.
Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, and Marc Vinyals.
Using Combinatorial Benchmarks to Probe the Reasoning Power of
Pseudo-Boolean Solvers.
In
Proceedings of the 21st International Conference on
Theory and Applications of Satisfiability Testing (SAT '18),
Lecture Notes in Computer Science, volume 10929,
pages 75-93, July 2018.
Marc Vinyals, Jan Elffers, Jesús Giráldez-Cru, Stephan Gocht, and Jakob Nordström.
In Between Resolution and Cutting Planes: A Study of Proof Systems
for Pseudo-Boolean SAT Solving.
In
Proceedings of the 21st International Conference on
Theory and Applications of Satisfiability Testing (SAT '18),
Lecture Notes in Computer Science, volume 10929,
pages 292-310, July 2018.
Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria,
Jakob Nordström, and Alexander Razborov.
Clique Is Hard on Average for Regular Resolution.
In
Proceedings of the 50th Annual ACM Symposium on Theory of Computing
(STOC '18),
pages 866-877, June 2018.
Massimo Lauria and Jakob Nordström.
Tight Size-Degree Bounds for Sums-of-Squares Proofs.Computational Complexity,
volume 26, issue 3, pages 911-948, December 2017.
Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals.
CNFgen: A Generator of Crafted Benchmarks.
In
Proceedings of the 20th International Conference on
Theory and Applications of Satisfiability Testing (SAT '17),
Lecture Notes in Computer Science, volume 10491,
pages 464-473, August 2017.
Massimo Lauria and Jakob Nordström.
Graph Colouring is Hard for Algorithms Based on
Hilbert's Nullstellensatz and Gröbner Bases.
In
Proceedings of the 32nd Annual Computational Complexity Conference (CCC '17),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 79, pages 2:1-2:20,
July 2017.
Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals.
Cumulative Space in Black-White Pebbling and Resolution.
In
Proceedings of the 8th Innovations in
Theoretical Computer Science Conference (ITCS '17),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 67, pages 38:1-38:21,
January 2017.
Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals.
How Limited Interaction Hinders Real Communication
(and What It Means for Proof and Circuit Complexity).
In
Proceedings of the 57th Annual IEEE Symposium on
Foundations of Computer Science (FOCS '16),
pages 295-304, October 2016.
Christoph Berkholz and Jakob Nordström.
Near-Optimal Lower Bounds on Quantifier Depth and
Weisfeiler-Leman Refinement Steps.
Technical Report TR16-135,
Electronic Colloquium on Computational Complexity (ECCC),
August 2016.
Christoph Berkholz and Jakob Nordström.
Supercritical Space-Width Trade-offs for Resolution.
In
Proceedings of the 43rd International Colloquium on
Automata, Languages and Programming (ICALP '16),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 55, pages 57:1-57:14, July 2016.
Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard,
Jakob Nordström, and Marc Vinyals.
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers.
In
Proceedings of the 19th International Conference on
Theory and Applications of Satisfiability Testing (SAT '16),
Lecture Notes in Computer Science, volume 9710,
pages 160-176, July 2016.
Christoph Berkholz and Jakob Nordström.
Near-Optimal Lower Bounds on Quantifier Depth and
Weisfeiler-Leman Refinement Steps.
In
Proceedings of the 31st Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS '16),
July 2016.
Albert Atserias, Massimo Lauria, and Jakob Nordström.
Narrow Proofs May Be Maximally Long.
In
ACM Transactions on Computational Logic,
volume 17, issue 3, article 19, May 2016.
Siu Man Chan, Massimo Lauria, Jakob Nordström, and Marc Vinyals.
Hardness of Approximation in PSPACE and Separation
Results for Pebble Games (Extended Abstract).
In
Proceedings of the 56th Annual IEEE Symposium on
Foundations of Computer Science (FOCS '15),
pages 466-485,
October 2015.
Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen.
Space Complexity in Polynomial Calculus.SIAM Journal on Computing,
volume 44, issue 4, pages 1119-1153, August 2015.
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals.
From Small Space to Small Width in Resolution.ACM Transactions on Computational Logic,
volume 16, issue 4, article 28, July 2015.
Massimo Lauria and Jakob Nordström.
Tight Size-Degree Bounds for Sums-of-Squares Proofs.
In
Proceedings of the 30th Annual
Computational Complexity Conference (CCC '15),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 33, pages 448-466,
June 2015.
Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
In
Proceedings of the 30th Annual
Computational Complexity Conference (CCC '15),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 33, pages 467-487,
June 2015.
Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
Technical Report TR15-078,
Electronic Colloquium on Computational Complexity (ECCC),
May 2015.
Mladen Mikša and Jakob Nordström.
Long Proofs of (Seemingly) Simple Formulas.
In
Proceedings of the 17th International Conference on
Theory and Applications of Satisfiability Testing (SAT '14),
Lecture Notes in Computer Science, volume 8561,
pages 121-137, July 2014.
Albert Atserias, Massimo Lauria, and Jakob Nordström.
Narrow Proofs May Be Maximally Long (Extended Abstract).
In
Proceedings of the 29th Annual IEEE Conference on Computational Complexity (CCC '14),
pages 286-297, June 2014.
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals.
From Small Space to Small Width in Resolution.
In
Proceedings of the 31st Symposium on Theoretical Aspects of Computer Science
(STACS '14),
pages 300-311, March 2014.
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, and Marc Vinyals.
Towards an Understanding of Polynomial Calculus: New Separations and
Lower Bounds (Extended Abstract).
In
Proceedings of the 40th International Colloquium on
Automata, Languages and Programming (ICALP '13),
Lecture Notes in Computer Science, volume 7965,
pages 437-448, July 2013.
Chris Beck, Jakob Nordström, and Bangsheng Tang.
Some Trade-off Results for Polynomial Calculus (Extended Abstract).
In
Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13),
pages 813-822,
June 2013.
Jakob Nordström and Johan Håstad.
Towards an Optimal Separation of Space and Length in Resolution.Theory of Computing,
volume 9, article 14, pages 471-557, May 2013.
Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný.
Relating Proof Complexity Measures and Practical Hardness of SAT.
In
Proceedings of the 18th International Conference on
Principles and Practice of Constraint Programming (CP '12),
Lecture Notes in Computer Science,
volume 7514, pages 316-331, October 2012.
Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga Ron-Zewi.
Space Complexity in Polynomial Calculus (Extended Abstract).
In
Proceedings of the 27th Annual IEEE Conference on Computational Complexity (CCC '12),
pages 334-344, June 2012.
Trinh Huynh and Jakob Nordström.
On the Virtue of Succinct Proofs:
Amplifying Communication Complexity Hardness to
Time-Space Trade-offs in Proof Complexity (Extended Abstract).
In
Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC '12),
pages 233-248, May 2012.
Jakob Nordström.
On the Relative Strength of Pebbling and Resolution.ACM Transactions on Computational Logic,
volume 13, issue 2, article 16, April 2012.
Arnab Bhattacharyya, Elena Grigorescu, Jakob Nordström, and Ning Xie.
On the Semantics of Local Characterizations for Linear-Invariant Properties.
Manuscript, 2011.
Jakob Nordström and Alexander Razborov.
On Minimal Unsatisfiability and
Time-Space Trade-offs for k-DNF Resolution.
In
Proceedings of the 38th International Colloquium on
Automata, Languages and Programming (ICALP '11),
Lecture Notes in Computer Science,
volume 6755, pages 642-653, July 2011.
Eli Ben-Sasson and Jakob Nordström.
Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions (Extended Abstract).
In
Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11),
pages 401-416, January 2011.
Eli Ben-Sasson and Jakob Nordström.
Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions.
Technical Report TR10-125,
Electronic Colloquium on Computational Complexity (ECCC),
August 2010.
Jakob Nordström.
On the Relative Strength of Pebbling and Resolution (Extended Abstract).
In
Proceedings of the 25th Annual IEEE Conference on
Computational Complexity (CCC '10),
pages 151-162, June 2010.
Jakob Nordström.
A Simplified Way of Proving Trade-off Results for Resolution.Information Processing Letters,
volume 109, number 18, pages 1030-1035, August 2009.
Jakob Nordström.
Narrow Proofs May Be Spacious: Separating Space and Width in Resolution.SIAM Journal on Computing,
volume 39, issue 1, pages 59-121, May 2009.
(Special issue for STOC '06.)
Eli Ben-Sasson and Jakob Nordström.
Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.
Technical Report TR09-002,
Electronic Colloquium on Computational Complexity (ECCC),
January 2009.
Eli Ben-Sasson and Jakob Nordström.
Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.
In
Proceedings of the 49th Annual IEEE Symposium on
Foundations of Computer Science (FOCS '08),
pages 709-718,
October 2008.
Jakob Nordström and Johan Håstad.
Towards an Optimal Separation of Space and Length in Resolution (Extended Abstract).
In
Proceedings of the 40th Annual ACM Symposium on Theory of Computing (STOC '08),
pages 701-710,
May 2008.
Jakob Nordström.
Narrow Proofs May Be Spacious: Separating Space and Width in Resolution (Extended Abstract).
In
Proceedings of the 38th Annual ACM Symposium on Theory of Computing (STOC '06),
pages 507-516,
May 2006.
Co-winner of the Danny Lewin Best Student Paper Award.
Survey Papers
Jakob Nordström.
New Wine into Old Wineskins: A Survey of Some
Pebbling Classics with Supplemental Results.
Manuscript in preparation.
To appear in
Foundations and Trends in Theoretical Computer Science.
Current draft version available for download—comments are welcome.
Sam Buss and Jakob Nordström.
Proof Complexity and SAT Solving.
In
Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (editors),
Handbook of Satisfiability, 2nd edition,
Chapter 7, pages 233-350. IOS Press, 2021.
Jakob Nordström.
On the Interplay Between Proof Complexity and SAT Solving.ACM SIGLOG News,
volume 2, number 3, pages 19-44, July 2015.
(Lightly edited version with some typos fixed.)
Jakob Nordström.
A (Biased) Proof Complexity Survey for SAT Practitioners.
In
Proceedings of the 17th International Conference on
Theory and Applications of Satisfiability Testing (SAT '14),
Lecture Notes in Computer Science, volume 8561,
pages 1-6, July 2014.
Jakob Nordström.
Pebble Games, Proof Complexity, and Time-Space Trade-offs.Logical Methods in Computer Science,
volume 9, issue 3, article 15, September 2013.
PhD Thesis
Jakob Nordström.
Short Proofs May Be Spacious: Understanding Space in Resolution.
PhD thesis,
Royal Institute of Technology,
Stockholm, Sweden, May 2008.
Received the Ackermann Award 2009
for outstanding dissertations in
Logic in Computer Science from the
European Association for Computer Science Logic.
Master's Thesis
Jakob Nordström.
Stålmarck's Method Versus Resolution: A Comparative Theoretical Study.
Master's thesis TRITA-NA-E0184,
Stockholm University,
Stockholm, Sweden,
2001.
Some Presentations
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.
Pseudo-Boolean 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,
March 2021.
(Also available in
video)
Pseudo-Boolean 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,
February 2021.
Slides for live talk
(with
video)
and slides for the longer version
(with pre-recorded 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 Size-Degree Trade-offs 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
Lower Bounds in Computational Complexity Reunion
workshop at the
Simons Institute for the Theory of Computing,
December 2019.
Learn to Relax: Integrating Integer Linear Programming
with Conflict-Driven 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 Pseudo-Width 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,
December 2018.
(Also available in
video)
Near-Optimal Lower Bounds on Quantifier Depth and
Weisfeiler-Leman Refinement Steps.
Talk given at the University of Copenhagen,
September 2018.
Divide and Conquer:
Towards Faster Conflict-Driven Pseudo-Boolean Solving.
Talk given at the University of Copenhagen,
September 2018.
Towards Faster Conflict-Driven Pseudo-Boolean 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
IJCAI-ECAI '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 Real-World 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 Space-Width Trade-offs for Resolution.
Talk given at the Dagstuhl seminar
Proof Complexity,
January-February 2018.
Lower Bound Techniques for Nullstellensatz and Polynomial Calculus.
Survey talk given at the Dagstuhl seminar
Proof Complexity,
January-February 2018.
Handwritten
notes
Understanding Conflict-Driven 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 Pseudo-Boolean 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 Conflict-Driven 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 Space-Width Trade-offs for Resolution.
Talk given at the Dagstuhl seminar
SAT and Interactions,
September 2016,
and at Rutgers University, New Jersey, USA,
October 2016.
Trade-offs 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.
Tutorial-style 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 SAT-lö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.
Time-Space Trade-offs 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
Time-Space Trade-offs 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.
Mini-Tutorial 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
from BIRS.)
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
Time-Space Trade-offs in Proof Complexity.
Talk given at the
Limits of Theorem Proving workshop in Rome, Italy, September 2012,
and (slightly modified) 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
Time-Space Trade-offs 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 time-space trade-offs in resolution and other proof systems
given at Stockholm University,
November 2011.
On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF 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,
June-July 2011,
and (slightly modified)
at the Oberwolfach workshop
Mathematical Logic: Proof Theory, Constructive Mathematics,
November 2011.
On the Semantics of Local Characterizations
for Linear-Invariant Properties.
Brief talk given at the Dagstuhl seminar on
Computational Complexity of Discrete Problems,
March 2011.
On the Semantics of Local Characterizations
for Linear-Invariant Properties.
Talk given
in the KTH Theory Group seminar series, November 2010,
and (slightly modified) 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 time-space trade-offs
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 Trade-offs 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 Trade-offs 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.
(Also available in
video
from Harvard.)
Understanding Space in Proof Complexity: Separations and Trade-offs 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 modified) 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 Trade-offs via Substitutions.
Brief overwiev talk
about the ECCC reports
TR09-034
and
TR09-047
given at the Barriers in Computational Complexity workshop in Princeton, USA, August 2009.
(Also available in video
from the Center for Computational Intractability.)
Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs.
Talk
about our
FOCS '08 paper
and
ECCC report TR09-034
given at the Dagstuhl seminar on
Computational Complexity of Discrete Problems,
September 2008,
and (slightly modified) 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 modified) at the Isaac Newton Institute Workshop
New Directions in Proof Complexity in Cambridge, UK, in April 2006.
(Also available in
audio
from the Isaac Newton Institute)
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.
Miscellaneous
[in Swedish] Jakob Nordström.
Kort populärvetenskaplig
sammanfattning av min doktorsavhandling.
Försök till kort (knappt 2 sidor)
sammanfattning av ungefär vad min doktorsavhandling handlar om
och varför man är intresserad av att undersöka
den typen av frågor,
september 2009.
[in Swedish] Jakob Nordström.
Om formler, bevis och andra komplexa saker.
Något förkortad och översatt version av inledningskapitlet
i min doktorsavhandling
Short Proofs May Be Spacious:
Understanding Space in Resolution,
maj 2008.