Publications
On this webpage you find my
research papers,
survey papers,
PhD thesis,
Master's thesis,
and
miscellaneous other stuff.
Everything should be sorted (at least roughly)
in reverse chronological order.
As a general rule, any published papers are copyright by their respective publishers but are free for personal use.
If you have any questions about any of my papers, then please feel free to
drop me a line.
Research Papers

Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
An Auditable Constraint Programming Solver.
To appear in
Proceedings of the 28th International Conference on
Principles and Practice of Constraint Programming (CP '22),
August 2022.

Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel.
Certified CNF Translations for PseudoBoolean Solving.
To appear in
Proceedings of the 25th International Conference on
Theory and Applications of Satisfiability Testing (SAT '22),
August 2022.

Daniela Kaufmann, Paul Beame, Armin Biere and Jakob Nordström.
Adding Dual Variables to Algebraic Reasoning for GateLevel Multiplier Verification.
In
Proceedings of the 25th
Design, Automation and Test in Europe Conference (DATE '22),
pages 14351440,
March 2022.

Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
Certified Symmetry and Dominance Breaking for Combinatorial Optimisation.
To appear in
Proceedings of the
36th AAAI Conference on Artificial Intelligence (AAAI '22),
February 2022.
Presented with a
Distinguished Paper Award.

Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
To appear in
Journal of the ACM, 2022.

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:123:26,
August 2021.

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:140: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 NPHard.
In
Proceedings of the 53rd Annual ACM Symposium on Theory of Computing
(STOC '21),
pages 209222,
June 2021.

Susanna F. de Rezende, Or Meir, Jakob Nordström, and Robert Robere.
Nullstellensatz SizeDegree Tradeoffs from Reversible Pebbling.
Computational Complexity,
volume 30, issue 1, pages 4:14:45, June 2021.

Jo Devriendt, Stephan Gocht, Emir Demirović,
Jakob Nordström, and Peter Stuckey.
Cutting to the Core of PseudoBoolean Optimization:
Combining CoreGuided Search with Cutting Planes Reasoning.
In
Proceedings of the
35th AAAI Conference on Artificial Intelligence (AAAI '21),
pages 37503758,
February 2021.

Stephan Gocht and Jakob Nordström.
Certifying Parity Reasoning Efficiently Using PseudoBoolean Proofs.
In
Proceedings of the
35th AAAI Conference on Artificial Intelligence (AAAI '21),
pages 37683777,
February 2021.

Jo Devriendt, Ambros Gleixner, and Jakob Nordström.
Learn to Relax: Integrating 01 Integer Linear Programming
with ConflictDriven PseudoBoolean 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 TR21006,
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 2430, 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 4349, November 2020.

Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, and Jakob Nordström.
Verifying Properties of Bitvector Multiplication
Using Cutting Planes Reasoning.
In
Proceedings of the 20th Conference on
Formal Methods in ComputerAided Design (FMCAD '20),
pages 194204, September 2020.

Jo Devriendt, Ambros Gleixner, and Jakob Nordström.
Learn to Relax: Integrating 01 Integer Linear Programming
with ConflictDriven PseudoBoolean Search.
In
Proceedings of the 17th International Conference on the
Integration of Constraint Programming, Artificial Intelligence,
and Operations Research (CPAIOR '20),
pages xxivxxv, 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 338357, 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 427444, 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 917934, 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:128:24,
July 2020.

Susanna F. de Rezende, Or Meir, Jakob Nordström,
Toniann Pitassi, and Robert Robere.
KRW Composition Theorems via Lifting.
Technical Report TR20099,
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 182200, 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 11341140,
July 2020.

Susanna F. de Rezende, Mika Göös, Jakob Nordström,
Toniann Pitassi, Robert Robere, and Dmitry Sokolov.
Automating Algebraic Proof Systems is NPHard.
Technical Report TR20064,
Electronic Colloquium on Computational Complexity (ECCC),
May 2020.

Christoph Berkholz and Jakob Nordström.
Supercritical SpaceWidth Tradeoffs for Resolution.
SIAM Journal on Computing,
volume 49, issue 1, pages 98118, February 2020.

Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
Justifying All Differences Using PseudoBoolean Reasoning.
In
Proceedings of the
34th AAAI Conference on Artificial Intelligence (AAAI '20),
pages 14861494,
February 2020.

Jan Elffers and Jakob Nordström.
A Cardinal Improvement to PseudoBoolean Solving.
In
Proceedings of the
34th AAAI Conference on Artificial Intelligence (AAAI '20),
pages 14951503,
February 2020.

Guillaume Lagarde, Jakob Nordström, Dmitry Sokolov, and Joseph Swernofsky.
Tradeoffs Between Size and Degree in Polynomial Calculus.
In
Proceedings of the 11th Innovations in
Theoretical Computer Science Conference (ITCS '20),
pages 72:172: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 TR19174,
Electronic Colloquium on Computational Complexity (ECCC),
December 2019.

Stephan Gocht, Jakob Nordström, and Amir Yehudayoff.
On Division Versus Saturation in PseudoBoolean Solving.
In
Proceedings of the 28th International Joint Conference on
Artificial Intelligence (IJCAI '19),
pages 17111718,
August 2019.

Susanna F. de Rezende,
Jakob Nordström,
Or Meir,
and Robert Robere.
Nullstellensatz SizeDegree Tradeoffs from
Reversible Pebbling.
In
Proceedings of the 34th Annual Computational Complexity Conference (CCC '19),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 137, pages 18:118:26,
July 2019.

Jan Elffers and Jakob Nordström.
Divide and Conquer: Towards Faster PseudoBoolean Solving.
In
Proceedings of the 27th International Joint Conference on
Artificial Intelligence (IJCAI '18),
pages 12911299, July 2018.

Jan Elffers, Jesús GiráldezCru, 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 13001308, July 2018.

Jan Elffers, Jesús GiráldezCru, Jakob Nordström, and Marc Vinyals.
Using Combinatorial Benchmarks to Probe the Reasoning Power of
PseudoBoolean 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 7593, July 2018.

Marc Vinyals, Jan Elffers, Jesús GiráldezCru, Stephan Gocht, and Jakob Nordström.
In Between Resolution and Cutting Planes: A Study of Proof Systems
for PseudoBoolean 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 292310, 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 866877, June 2018.

Massimo Lauria and Jakob Nordström.
Tight SizeDegree Bounds for SumsofSquares Proofs.
Computational Complexity,
volume 26, issue 3, pages 911948, 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 464473, 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:12:20,
July 2017.

Joël Alwen, Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals.
Cumulative Space in BlackWhite 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:138: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 295304, October 2016.

Christoph Berkholz and Jakob Nordström.
NearOptimal Lower Bounds on Quantifier Depth and
WeisfeilerLeman Refinement Steps.
Technical Report TR16135,
Electronic Colloquium on Computational Complexity (ECCC),
August 2016.

Christoph Berkholz and Jakob Nordström.
Supercritical SpaceWidth Tradeoffs 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:157:14, July 2016.

Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard,
Jakob Nordström, and Marc Vinyals.
Tradeoffs 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 160176, July 2016.

Christoph Berkholz and Jakob Nordström.
NearOptimal Lower Bounds on Quantifier Depth and
WeisfeilerLeman 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 466485,
October 2015.

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga RonZewi, and Neil Thapen.
Space Complexity in Polynomial Calculus.
SIAM Journal on Computing,
volume 44, issue 4, pages 11191153, 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 SizeDegree Bounds for SumsofSquares Proofs.
In
Proceedings of the 30th Annual
Computational Complexity Conference (CCC '15),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 33, pages 448466,
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 467487,
June 2015.

Mladen Mikša and Jakob Nordström.
A Generalized Method for Proving
Polynomial Calculus Degree Lower Bounds.
Technical Report TR15078,
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 121137, 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 286297, 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 300311, 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 437448, July 2013.

Chris Beck, Jakob Nordström, and Bangsheng Tang.
Some Tradeoff Results for Polynomial Calculus (Extended Abstract).
In
Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13),
pages 813822,
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 471557, 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 316331, October 2012.

Yuval Filmus, Massimo Lauria, Jakob Nordström, Neil Thapen, and Noga RonZewi.
Space Complexity in Polynomial Calculus (Extended Abstract).
In
Proceedings of the 27th Annual IEEE Conference on Computational Complexity (CCC '12),
pages 334344, June 2012.

Trinh Huynh and Jakob Nordström.
On the Virtue of Succinct Proofs:
Amplifying Communication Complexity Hardness to
TimeSpace Tradeoffs in Proof Complexity (Extended Abstract).
In
Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC '12),
pages 233248, 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 LinearInvariant Properties.
Manuscript, 2011.

Jakob Nordström and Alexander Razborov.
On Minimal Unsatisfiability and
TimeSpace Tradeoffs for kDNF Resolution.
In
Proceedings of the 38th International Colloquium on
Automata, Languages and Programming (ICALP '11),
Lecture Notes in Computer Science,
volume 6755, pages 642653, July 2011.

Eli BenSasson and Jakob Nordström.
Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions (Extended Abstract).
In
Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11),
pages 401416, January 2011.

Eli BenSasson and Jakob Nordström.
Understanding Space in Proof Complexity: Separations and Tradeoffs via Substitutions.
Technical Report TR10125,
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 151162, June 2010.

Jakob Nordström.
A Simplified Way of Proving Tradeoff Results for Resolution.
Information Processing Letters,
volume 109, number 18, pages 10301035, 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 59121, May 2009.
(Special issue for STOC '06.)

Eli BenSasson and Jakob Nordström.
Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution.
Technical Report TR09002,
Electronic Colloquium on Computational Complexity (ECCC),
January 2009.

Eli BenSasson 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 709718,
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 701710,
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 507516,
May 2006.
Cowinner 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 233350. IOS Press, 2021.

Jakob Nordström.
On the Interplay Between Proof Complexity and SAT Solving.
ACM SIGLOG News,
volume 2, number 3, pages 1944, 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 16, July 2014.

Jakob Nordström.
Pebble Games, Proof Complexity, and TimeSpace Tradeoffs.
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 TRITANAE0184,
Stockholm University,
Stockholm, Sweden,
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.
