| 2026 | AAAI | Faster Certified Symmetry Breaking Using Orders with Auxiliary Variables. | Markus Anders, Bart Bogaerts, Benjamin Bog, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Adrian Rebola-Pardo, Yong Kiam Tan |
| 2026 | CP | End-to-End Certified Graph Colouring. | Simon Dold, George Katsirelos, Wietze Koops, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan |
| 2026 | CP | Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB. | Ciaran McCreesh, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan |
| 2025 | CP | Practically Feasible Proof Logging for Pseudo-Boolean Optimization. | Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan, Marc Vinyals |
| 2025 | ICAPS | Pseudo-Boolean Proof Logging for Optimal Classical Planning. | Simon Dold, Malte Helmert, Jakob Nordstrm, Gabriele Rger, Tanja Schindler |
| 2025 | STOC | Truly Supercritical Trade-Offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman. | Susanna F. de Rezende, Noah Fleming, Duri Andrea Janett, Jakob Nordstrm, Shuo Pang |
| 2024 | AAAI | End-to-End Verification for Subgraph Solving. | Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordstrm, Andy Oertel, Yong Kiam Tan |
| 2024 | CP | Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. | Jeremias Berg, Bart Bogaerts, Jakob Nordstrm, Andy Oertel, Tobias Paxian, Dieter Vandesande |
| 2024 | CP | Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms. | Emir Demirovic, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordstrm, Andy Oertel, Konstantin Sidorov |
| 2024 | CPAIOR | Certifying MIP-Based Presolve Reductions for 0-1 Integer Linear Programs. | Alexander Hoen, Andy Oertel, Ambros M. Gleixner, Jakob Nordstrm |
| 2024 | CPAIOR | Proof Logging for the Circuit Constraint. | Matthew J. McIlree, Ciaran McCreesh, Jakob Nordstrm |
| 2024 | IJCAR | Certified MaxSAT Preprocessing. | Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Jrvisalo, Magnus O. Myreen, Jakob Nordstrm |
| 2023 | CADE | Certified Core-Guided MaxSAT Solving. | Jeremias Berg, Bart Bogaerts, Jakob Nordstrm, Andy Oertel, Dieter Vandesande |
| 2023 | CP | Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. | Gioni Mexi, Timo Berthold, Ambros M. Gleixner, Jakob Nordstrm |
| 2023 | FOCS | Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz. | Jonas Conneryd, Susanna F. de Rezende, Jakob Nordstrm, Shuo Pang, Kilian Risse |
| 2023 | IJCAI | Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract). | Stephan Gocht, Ruben Martins, Jakob Nordstrm, Andy Oertel |
| 2022 | AAAI | Certified Symmetry and Dominance Breaking for Combinatorial Optimisation. | Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, Jakob Nordstrm |
| 2022 | CP | An Auditable Constraint Programming Solver. | Stephan Gocht, Ciaran McCreesh, Jakob Nordstrm |
| 2022 | DATE | Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. | Daniela Kaufmann, Paul Beame, Armin Biere, Jakob Nordstrm |
| 2022 | SAT | Certified CNF Translations for Pseudo-Boolean Solving. | Stephan Gocht, Ruben Martins, Jakob Nordstrm, Andy Oertel |
| 2021 | AAAI | Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning. | Jo Devriendt, Stephan Gocht, Emir Demirovic, Jakob Nordstrm, Peter J. Stuckey |
| 2021 | AAAI | Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs. | Stephan Gocht, Jakob Nordstrm |
| 2021 | STOC | Automating algebraic proof systems is NP-hard. | Susanna F. de Rezende, Mika Gs, Jakob Nordstrm, Toniann Pitassi, Robert Robere, Dmitry Sokolov |
| 2020 | AAAI | Justifying All Differences Using Pseudo-Boolean Reasoning. | Jan Elffers, Stephan Gocht, Ciaran McCreesh, Jakob Nordstrm |
| 2020 | AAAI | A Cardinal Improvement to Pseudo-Boolean Solving. | Jan Elffers, Jakob Nordstrm |
| 2020 | CP | Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems. | Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordstrm, Patrick Prosser, James Trimble |
| 2020 | CP | Using Resolution Proofs to Analyse CDCL Solvers. | Janne I. Kokkala, Jakob Nordstrm |
| 2020 | CP | Theoretical and Experimental Results for Planning with Learned Binarized Neural Network Transition Models. | Buser Say, Jo Devriendt, Jakob Nordstrm, Peter J. Stuckey |
| 2020 | FMCAD | Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. | Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, Jakob Nordstrm |
| 2020 | FOCS | KRW Composition Theorems via Lifting. | Susanna F. de Rezende, Or Meir, Jakob Nordstrm, Toniann Pitassi, Robert Robere |
| 2020 | FOCS | Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. | Susanna F. de Rezende, Or Meir, Jakob Nordstrm, Toniann Pitassi, Robert Robere, Marc Vinyals |
| 2020 | IJCAI | Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions. | Stephan Gocht, Ciaran McCreesh, Jakob Nordstrm |
| 2020 | SAT | Simplified and Improved Separations Between Regular and General Resolution by Lifting. | Marc Vinyals, Jan Elffers, Jan Johannsen, Jakob Nordstrm |
| 2019 | IJCAI | On Division Versus Saturation in Pseudo-Boolean Solving. | Stephan Gocht, Jakob Nordstrm, Amir Yehudayoff |
| 2018 | IJCAI | Seeking Practical CDCL Insights from Theoretical SAT Benchmarks. | Jan Elffers, Jess Girldez-Cru, Stephan Gocht, Jakob Nordstrm, Laurent Simon |
| 2018 | IJCAI | Divide and Conquer: Towards Faster Pseudo-Boolean Solving. | Jan Elffers, Jakob Nordstrm |
| 2018 | STOC | Clique is hard on average for regular resolution. | Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordstrm, Alexander A. Razborov |
| 2018 | SAT | Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers. | Jan Elffers, Jess Girldez-Cru, Jakob Nordstrm, Marc Vinyals |
| 2018 | SAT | In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving. | Marc Vinyals, Jan Elffers, Jess Girldez-Cru, Stephan Gocht, Jakob Nordstrm |
| 2017 | SAT | CNFgen: A Generator of Crafted Benchmarks. | Massimo Lauria, Jan Elffers, Jakob Nordstrm, Marc Vinyals |
| 2016 | FOCS | How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity). | Susanna F. de Rezende, Jakob Nordstrm, Marc Vinyals |
| 2016 | ICALP | Supercritical Space-Width Trade-Offs for Resolution. | Christoph Berkholz, Jakob Nordstrm |
| 2016 | LICS | Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. | Christoph Berkholz, Jakob Nordstrm |
| 2016 | SAT | Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. | Jan Elffers, Jan Johannsen, Massimo Lauria, Thomas Magnard, Jakob Nordstrm, Marc Vinyals |
| 2015 | FOCS | Hardness of Approximation in PSPACE and Separation Results for Pebble Games. | Siu Man Chan, Massimo Lauria, Jakob Nordstrm, Marc Vinyals |
| 2014 | STACS | From Small Space to Small Width in Resolution. | Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordstrm, Marc Vinyals |
| 2014 | SAT | Long Proofs of (Seemingly) Simple Formulas. | Mladen Miksa, Jakob Nordstrm |
| 2014 | SAT | A (Biased) Proof Complexity Survey for SAT Practitioners. | Jakob Nordstrm |
| 2013 | ICALP | Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds - (Extended Abstract). | Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordstrm, Marc Vinyals |
| 2013 | STOC | Some trade-off results for polynomial calculus: extended abstract. | Chris Beck, Jakob Nordstrm, Bangsheng Tang |
| 2012 | CP | Relating Proof Complexity Measures and Practical Hardness of SAT. | Matti Jrvisalo, Arie Matsliah, Jakob Nordstrm, Stanislav Zivn |
| 2012 | STOC | On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity. | Trinh Huynh, Jakob Nordstrm |
| 2011 | ICALP | On Minimal Unsatisfiability and Time-Space Trade-offs for | Jakob Nordstrm, Alexander A. Razborov |
| 2008 | FOCS | Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution. | Eli Ben-Sasson, Jakob Nordstrm |
| 2008 | STOC | Towards an optimal separation of space and length in resolution. | Jakob Nordstrm, Johan Hstad |
| 2006 | STOC | Narrow proofs may be spacious: separating space and width in resolution. | Jakob Nordstrm |