Towards an Optimal Separation of Space and Length in Resolution. - Jakob Nordström; Johan Håstad (Electron. Colloquium Comput. Complex., 2008)

Short Proofs May Be Spacious : Understanding Space in Resolution. - Jakob Nordström (2008)

Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution. - Eli Ben-Sasson; Jakob Nordström (Electron. Colloquium Comput. Complex., 2009)

Understanding Space in Resolution: Optimal Lower Bounds and Exponential Trade-offs. - Eli Ben-Sasson; Jakob Nordström (Electron. Colloquium Comput. Complex., 2009)

A Space Hierarchy for k-DNF Resolution. - Eli Ben-Sasson; Jakob Nordström (Electron. Colloquium Comput. Complex., 2009)

On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution. - Jakob Nordström; Alexander A. Razborov (Electron. Colloquium Comput. Complex., 2009)

A simplified way of proving trade-off results for resolution. - Jakob Nordström (Inf. Process. Lett., 2009)

Narrow Proofs May Be Spacious: Separating Space and Width in Resolution. - Jakob Nordström (SIAM J. Comput., 2009)

Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions. - Eli Ben-Sasson; Jakob Nordström (Electron. Colloquium Comput. Complex., 2010)

Separations of Matroid Freeness Properties. - Arnab Bhattacharyya 001; Elena Grigorescu; Jakob Nordström; Ning Xie 002 (Electron. Colloquium Comput. Complex., 2010)

On the Relative Strength of Pebbling and Resolution. - Jakob Nordström (Electron. Colloquium Comput. Complex., 2010)

On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution. - Jakob Nordström; Alexander A. Razborov (ICALP (1), 2011)

Relating Proof Complexity Measures and Practical Hardness of SAT. - Matti Järvisalo; Arie Matsliah; Jakob Nordström; Stanislav Zivný (CP, 2012)

On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity. - Trinh Huynh; Jakob Nordström (STOC, 2012)

Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds - (Extended Abstract). - Yuval Filmus; Massimo Lauria; Mladen Miksa; Jakob Nordström; Marc Vinyals (ICALP (1), 2013)

Some trade-off results for polynomial calculus: extended abstract. - Chris Beck; Jakob Nordström; Bangsheng Tang (STOC, 2013)

Pebble Games, Proof Complexity, and Time-Space Trade-offs. - Jakob Nordström (Log. Methods Comput. Sci., 2013)

Long Proofs of (Seemingly) Simple Formulas. - Mladen Miksa; Jakob Nordström (SAT, 2014)

A (Biased) Proof Complexity Survey for SAT Practitioners. - Jakob Nordström (SAT, 2014)

Narrow Proofs May Be Maximally Long. - Albert Atserias; Massimo Lauria; Jakob Nordström (Electron. Colloquium Comput. Complex., 2014)

From Small Space to Small Width in Resolution. - Yuval Filmus; Massimo Lauria; Mladen Miksa; Jakob Nordström; Marc Vinyals (Electron. Colloquium Comput. Complex., 2014)

Hardness of Approximation in PSPACE and Separation Results for Pebble Games. - Siu Man Chan; Massimo Lauria; Jakob Nordström; Marc Vinyals (FOCS, 2015)

Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). - Armin Biere; Vijay Ganesh 001; Martin Grohe; Jakob Nordström; Ryan Williams 001 (Dagstuhl Reports, 2015)

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds. - Mladen Miksa; Jakob Nordström (Electron. Colloquium Comput. Complex., 2015)

Space Complexity in Polynomial Calculus. - Yuval Filmus; Massimo Lauria; Jakob Nordström; Noga Ron-Zewi; Neil Thapen (SIAM J. Comput., 2015)

On the interplay between proof complexity and SAT solving. - Jakob Nordström (ACM SIGLOG News, 2015)

Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers. - Jan Elffers; Jan Johannsen; Massimo Lauria; Thomas Magnard; Jakob Nordström; Marc Vinyals (SAT, 2016)

Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. - Christoph Berkholz; Jakob Nordström (Electron. Colloquium Comput. Complex., 2016)

Graph Colouring is Hard for Algorithms Based on Hilbert's Nullstellensatz and Gröbner Bases. - Massimo Lauria; Jakob Nordström (CCC, 2017)

Cumulative Space in Black-White Pebbling and Resolution. - Joël Alwen; Susanna F. de Rezende; Jakob Nordström; Marc Vinyals (ITCS, 2017)

CNFgen: A Generator of Crafted Benchmarks. - Massimo Lauria; Jan Elffers; Jakob Nordström; Marc Vinyals (SAT, 2017)

Tight Size-Degree Bounds for Sums-of-Squares Proofs. - Massimo Lauria; Jakob Nordström (Comput. Complex., 2017)

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks. - Jan Elffers; Jesús Giráldez-Cru; Stephan Gocht; Jakob Nordström; Laurent Simon 001 (IJCAI, 2018)

Divide and Conquer: Towards Faster Pseudo-Boolean Solving. - Jan Elffers; Jakob Nordström (IJCAI, 2018)

Using Combinatorial Benchmarks to Probe the Reasoning Power of Pseudo-Boolean Solvers. - Jan Elffers; Jesús Giráldez-Cru; Jakob Nordström; Marc Vinyals (SAT, 2018)

In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving. - Marc Vinyals; Jan Elffers; Jesús Giráldez-Cru; Stephan Gocht; Jakob Nordström (SAT, 2018)

Proof Complexity (Dagstuhl Seminar 18051). - Albert Atserias; Jakob Nordström; Pavel Pudlák; Rahul Santhanam (Dagstuhl Reports, 2018)

On Division Versus Saturation in Pseudo-Boolean Solving. - Stephan Gocht; Jakob Nordström; Amir Yehudayoff (IJCAI, 2019)

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. - Or Meir; Jakob Nordström; Toniann Pitassi; Robert Robere; Susanna F. de Rezende (Electron. Colloquium Comput. Complex., 2019)

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs. - Susanna F. de Rezende; Jakob Nordström; Kilian Risse; Dmitry Sokolov 001 (Electron. Colloquium Comput. Complex., 2019)

Justifying All Differences Using Pseudo-Boolean Reasoning. - Jan Elffers; Stephan Gocht; Ciaran McCreesh; Jakob Nordström (AAAI, 2020)

A Cardinal Improvement to Pseudo-Boolean Solving. - Jan Elffers; Jakob Nordström (AAAI, 2020)

Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems. - Stephan Gocht; Ross McBride; Ciaran McCreesh; Jakob Nordström; Patrick Prosser; James Trimble 001 (CP, 2020)

Using Resolution Proofs to Analyse CDCL Solvers. - Janne I. Kokkala; Jakob Nordström (CP, 2020)

Theoretical and Experimental Results for Planning with Learned Binarized Neural Network Transition Models. - Buser Say; Jo Devriendt; Jakob Nordström; Peter J. Stuckey (CP, 2020)

Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning. - Vincent Liew; Paul Beame; Jo Devriendt; Jan Elffers; Jakob Nordström (FMCAD, 2020)

Lifting with Simple Gadgets and Applications to Circuit and Proof Complexity. - Susanna F. de Rezende; Or Meir; Jakob Nordström; Toniann Pitassi; Robert Robere; Marc Vinyals (FOCS, 2020)

Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions. - Stephan Gocht; Ciaran McCreesh; Jakob Nordström (IJCAI, 2020)

Trade-Offs Between Size and Degree in Polynomial Calculus. - Guillaume Lagarde; Jakob Nordström; Dmitry Sokolov 001; Joseph Swernofsky (ITCS, 2020)

Simplified and Improved Separations Between Regular and General Resolution by Lifting. - Marc Vinyals; Jan Elffers; Jan Johannsen; Jakob Nordström (SAT, 2020)

Automating Algebraic Proof Systems is NP-Hard. - Mika Göös; Jakob Nordström; Toniann Pitassi; Robert Robere; Dmitry Sokolov 001; Susanna F. de Rezende (Electron. Colloquium Comput. Complex., 2020)

Supercritical Space-Width Trade-offs for Resolution. - Christoph Berkholz; Jakob Nordström (SIAM J. Comput., 2020)

Experimental Repository for "Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning". - Jo Devriendt; Stephan Gocht; Emir Demirovic; Jakob Nordström; Peter J. Stuckey (Zenodo, 2020)

Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning. - Jo Devriendt; Stephan Gocht; Emir Demirovic; Jakob Nordström; Peter J. Stuckey (AAAI, 2021)

Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs. - Stephan Gocht; Jakob Nordström (AAAI, 2021)

The Power of Negative Reasoning. - Susanna F. de Rezende; Massimo Lauria; Jakob Nordström; Dmitry Sokolov 001 (CCC, 2021)

Certifying CNF Encodings of Pseudo-Boolean Constraints (abstract). - Stephan Gocht; Jakob Nordström; Ruben Martins (PxTP, 2021)

Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. - Susanna F. de Rezende; Or Meir; Jakob Nordström; Robert Robere (Comput. Complex., 2021)

Learn to relax: Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search. - Jo Devriendt; Ambros M. Gleixner; Jakob Nordström (Constraints An Int. J., 2021)

Planning with Learned Binarized Neural Networks Benchmarks for MaxSAT Evaluation 2021. - Buser Say; Scott Sanner; Jo Devriendt; Jakob Nordström; Peter J. Stuckey (CoRR, 2021)

How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity). - Susanna F. de Rezende; Jakob Nordström; Marc Vinyals (Electron. Colloquium Comput. Complex., 2021)

Clique Is Hard on Average for Regular Resolution. - Albert Atserias; Ilario Bonacina; Susanna F. de Rezende; Massimo Lauria; Jakob Nordström; Alexander A. Razborov (J. ACM, 2021)

Proof Complexity and SAT Solving. - Sam Buss; Jakob Nordström (Handbook of Satisfiability, 2021)

Certified Symmetry and Dominance Breaking for Combinatorial Optimisation. - Bart Bogaerts 001; Stephan Gocht; Ciaran McCreesh; Jakob Nordström (AAAI, 2022)

An Auditable Constraint Programming Solver. - Stephan Gocht; Ciaran McCreesh; Jakob Nordström (CP, 2022)

Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. - Daniela Kaufmann; Paul Beame; Armin Biere; Jakob Nordström (DATE, 2022)

Certified CNF Translations for Pseudo-Boolean Solving. - Stephan Gocht; Ruben Martins; Jakob Nordström; Andy Oertel (SAT, 2022)

Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). - Olaf Beyersdorff; Armin Biere; Vijay Ganesh 001; Jakob Nordström; Andy Oertel (Dagstuhl Reports, 2022)

Certified Core-Guided MaxSAT Solving. - Jeremias Berg; Bart Bogaerts 001; Jakob Nordström; Andy Oertel; Dieter Vandesande (CADE, 2023)

Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. - Gioni Mexi; Timo Berthold; Ambros M. Gleixner; Jakob Nordström (CP, 2023)

Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract). - Stephan Gocht; Ruben Martins; Jakob Nordström; Andy Oertel (IJCAI, 2023)

Certified Dominance and Symmetry Breaking for Combinatorial Optimisation. - Bart Bogaerts 001; Stephan Gocht; Ciaran McCreesh; Jakob Nordström (J. Artif. Intell. Res., 2023)

End-to-End Verification for Subgraph Solving. - Stephan Gocht; Ciaran McCreesh; Magnus O. Myreen; Jakob Nordström; Andy Oertel; Yong Kiam Tan (AAAI, 2024)

Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. - Jeremias Berg; Bart Bogaerts 001; Jakob Nordström; Andy Oertel; Tobias Paxian; Dieter Vandesande (CP, 2024)

Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms. - Emir Demirovic; Ciaran McCreesh; Matthew J. McIlree; Jakob Nordström; Andy Oertel; Konstantin Sidorov (CP, 2024)

Certifying MIP-Based Presolve Reductions for 0-1 Integer Linear Programs. - Alexander Hoen; Andy Oertel; Ambros M. Gleixner; Jakob Nordström (CPAIOR (1), 2024)

Proof Logging for the Circuit Constraint. - Matthew J. McIlree; Ciaran McCreesh; Jakob Nordström (CPAIOR (2), 2024)

Certified MaxSAT Preprocessing. - Hannes Ihalainen; Andy Oertel; Yong Kiam Tan; Jeremias Berg; Matti Järvisalo; Magnus O. Myreen; Jakob Nordström (IJCAR (1), 2024)

Certified MaxSAT Preprocessing. - Hannes Ihalainen; Andy Oertel; Yong Kiam Tan; Jeremias Berg; Matti Järvisalo; Jakob Nordström (CoRR, 2024)

Truly Supercritical Trade-offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman. - Susanna F. de Rezende; Noah Fleming; Duri Andrea Janett; Jakob Nordström; Shuo Pang 002 (Electron. Colloquium Comput. Complex., 2024)

KRW Composition Theorems via Lifting. - Susanna F. de Rezende; Or Meir; Jakob Nordström; Toniann Pitassi; Robert Robere (Comput. Complex., 2024)

Practically Feasible Proof Logging for Pseudo-Boolean Optimization. - Wietze Koops; Daniel Le Berre; Magnus O. Myreen; Jakob Nordström; Andy Oertel; Yong Kiam Tan; Marc Vinyals (CP, 2025)

Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz. - Jonas Conneryd; Susanna F. de Rezende; Jakob Nordström; Shuo Pang 002; Kilian Risse (Electron. Colloquium Comput. Complex., 2025)

Pseudo-Boolean Proof Logging for Optimal Classical Planning. - Simon Dold 001; Malte Helmert; Jakob Nordström; Gabriele Röger; Tanja Schindler (CoRR, 2025)