Mathematical Insights into Algorithms for Optimization (MIAO) Group

Some Highlights

We are hiring! Please check out the open positions webpage for news about current and/or upcoming openings.
A big welcome to our new PhD student Rui Ji!
In March 2024 most of the research group had the pleasure of attending the workshop Proof Complexity and Beyond at Mathematisches Forschungsinstitut Oberwolfach, organized by Jakob Nordström together with Albert Atserias, Meena Mahajan, and Alexander Razborov.
At the constraint programming conference CP '23, former MIAO PhD student Stephan Gocht received the ACP Doctoral Research Award from the Association for Constraint Programming for his work on proof logging. Not only that, but our close collaborator Ciaran McCreesh received the ACP Early Career Researcher Award, among other things for our joint work on proof logging, and Ciaran and his PhD student Matthew McIlree got the CP 2023 best paper award for their work on proof logging for constraint programming solvers using VeriPB. So, all in all, a pretty good week for certifying combinatorial solvers…
At the AI conference IJCAI '23, we gave a tutorial Combinatorial Solving with Provably Correct Results on VeriPB proof logging.
The SAT solver with VeriPB proof logging, BreakID-kissat-low, that we submitted to the SAT Competition 2023 was the most successful solver in the competition, and would have won 1st prize had the competition rules been like in previous years. With VeriPB proof logging we can support advanced SAT solving techniques that have previously been out of reach for the standard SAT proof logging format, thus increasing the power of the solver exponentially. However, our proof checking is still not as fast as in the highly optimized checkers for the standard format that have been used for the last decade, and some of our proofs were not verified within the required time limits. Therefore, we instead had to to content ourselves with receiving an honorary 1st prize. We know how to make our toolchain for formal verification of proofs more efficient, though, and are working on it for next year—and it is already clear what is the future of efficient, powerful, fully general SAT proof logging…
Our pseudo-Boolean proof checker VeriPB was used as one of the official proof checkers in the SAT Competition 2023. (See the VeriPB tutorial with accompanying slides for more information about everything else that this tool can support.)
During the spring of 2023 we had the pleasure of attending the Meta-Complexity program and the extended reunion of the program Satisfiability: Theory, Practice, and Beyond at the Simons Institute for the Theory of Computing at UC Berkeley.
In December 2022 we gave a series of lectures on pseudo-Boolean solving and optimization at the Indian SAT+SMT Winter School at IIT Madras in Chennai. There are video recordings of part 1, part 2, part 3, and part 4 of the tutorial, as well as of the demo session.
Our paper Certified CNF Translations for Pseudo-Boolean Solving. by Stephan Gocht, Andy Oertel, and Jakob Nordström from the MIAO group joint with Ruben Martins received a SAT '22 best paper award.
Our paper Certified Symmetry and Dominance Breaking for Combinatorial Optimisation by Stephan Gocht and Jakob Nordström from the MIAO group joint with Bart Bogaerts and Ciaran McCreesh received a AAAI '22 distinguished paper award.

About the MIAO Research Group

The Mathematical Insights into Algorithms for Optimization (MIAO) research group is based on both sides of the Öresund Bridge at Lund University and the University of Copenhagen. We are closely affiliated with the Basic Algorithms Research Copenhagen (BARC) centre, and are part of a world-leading environment in algorithms and complexity theory encompassing also the IT University of Copenhagen and the Technical University of Denmark (DTU). We aim to attract top talent from around the world to an ambitious, creative, collaborative, and fun environment. Using the power of mathematics, we strive to create fundamental breakthroughs in algorithms and complexity theory. While the focus in on foundational research, algorithms and complexity researchers in Copenhagen have a track record of surprising algorithmic discoveries leading to major industrial applications.

The MIAO research group has a unique profile in that we are doing cutting-edge research both on the mathematical foundations of efficient computation and on state-of-the-art practical algorithms for real-world problems. This creates a very special environment, where we do not only conduct in-depth research on different theoretical and applied topics, but where different lines of research cross-fertilise each other and unexpected and exciting synergies often arise. Much of the activities of the group revolve around powerful algorithmic paradigms such as, e.g., Boolean satisfiability (SAT) solving, Gröbner basis computations, integer linear programming, and constraint programming. This leads to classical questions in computational complexity theory—though often with new, fascinating twists—but also involves work on devising clever algorithms that can exploit the power of such paradigms in practice.

On the theory side, most of our work has been in proof complexity, i.e., the study of formal systems for reasoning about logic formulas and other types of problems from the point of view of computational complexity. Proof complexity has connections to foundational questions in computational complexity theory, but another important motivation is algorithm analysis. All algorithms use some kind of method of reasoning to compute solutions to problems, and proof complexity can be used to analyse the potential and limitations of such methods (and thereby of the algorithms using them). As often happens in theoretical computer science, our research in proof complexity has revealed deep, and often quite surprising, connections to other areas such as, e.g., circuit complexity, communication complexity, hardness of approximation, and finite model theory, and so we are also interested in such areas. See the slides for the talk Proof Complexity and SAT Solving for an overview of this area (with a bias towards connections to algorithms).

On the practical side, we want to gain a more rigorous scientific understanding, and improve the efficiency, of modern algorithms for automated reasoning and combinatorial optimization. We are particularly interested in designing algorithms that can exploit sophisticated mathematical techniques to achieve exponential improvements in performance compared to the current state of the art—something that theoretical research suggests should be possible, but that has so far been hard to achieve in practice. Combining ideas from SAT solving and mixed integer linear programming (MIP), we have constructed a new 0-1 integer linear programming solver RoundingSat. This solver is already world-leading when it comes to pseudo-Boolean solving, but our goal is to develop it further, integrating ideas also from MaxSAT solving, MIP solving, and possibly also constraint programming (CP), ultimately hoping to go significantly beyond the current state of the art. For more information about this line of research, see the Indian SAT+SMT Winter School 2022 lectures on SAT solving, pseudo-Boolean solving, pseudo-Boolean optimization, and mixed integer linear programming and pseudo-Boolean solving/optimization, as well as the demo session (with slides for part 1 PDF , part 2 PDF , part 3 PDF , and part 4 PDF of the lectures).

In the last few years we have also made research breakthroughs on how to verify the correctness of state-of-the-art algorithms for combinatorial solving and optimization. Such algorithms are often highly complex, and even mature commercial solvers are known to sometimes produce wrong results. Our goal is to usher in a new generation of certifying combinatorial solvers with so-called proof logging, meaning that the solvers output not only a result but also a simple, machine-verifiable proof that the claimed result is correct. For such a certifying solver, the workflow becomes as follows:

Run the solver on a problem instance to obtain not only a computed result, but also a proof of correctness.
Feed the problem, the result, and the proof of correctness to a special, dedicated proof checker for verification.
Accept the result if the proof checker says that the proof is valid.

Importantly, these machine-verifiable proofs should be very easy to generate and should require low overhead on the solver side, but should also be very easy to check efficiently on the proof checker side, and should still provide 100% formal guarantees of correctness. This might sound just a little bit too good to be true, but the tool VeriPB that we have developed can now provide efficient proof logging for several combinatorial solving paradigms that have previously been beyond reach, and we have recently received several prestigious awards for our work. VeriPB was also used as one of the proof checkers in the SAT Competition 2023, allowing solver authors for the first time to use also the most advanced SAT techniques (such as Gaussian elimination and fully general symmetry breaking) that have lacked efficient support in previous SAT proof logging tools. See our video tutorial Combinatorial solving with provably correct results with accompanying slides PDF for more details.

Principal Investigator

Jakob Nordström, professor at the University of Copenhagen and Lund University

Researchers

The MIAO group has the pleasure of collaborating closely with Susanna F. de Rezende, and all PhD students in Copenhagen and Lund are jointly advised by Susanna and Jakob regardless of their sources of funding.

Shuo Pang, postdoctoral researcher (since 2022)
Noel Arteche, PhD student (since 2022)
Jonas Conneryd, PhD student (since 2021)
Yassine Ghannane, PhD student (since 2023)
Duri Andrea Janett, PhD student (since 2023)
Rui Ji, PhD student (since April 2024)
Maryia Kapytka, PhD student (starting in the spring of 2024)
Wietze Koops, PhD student (starting in September 2024)
Andy Oertel, PhD student (since 2021)

Friends of MIAO

We are fortunate to be able to interact closely with several researchers in computational complexity theory at Lund University, the University of Copenhagen, and the IT University of Copenhagen:

Susanna F. de Rezende, assistant professor at the Department of Computer Science at Lund University
Paloma T. Lima, assistant professor at the IT University of Copenhagen
Nutan Limaye, associate professor at the IT University of Copenhagen
Srikanth Srinivasan, associate professor at the University of Copenhagen
Amir Yehudayoff, professor at the University of Copenhagen

BSc and MSc Students (Current and Former)

Alexander Miller-Murphy, University of Toronto, undergraduate summer research intern at Lund University, 2022
Cody Dempster, University of Michigan, undergraduate summer research intern at Lund University, 2022
Ziyang Men, MSc student, University of Copenhagen, 2022
Jonatan Nilsson, Lund University, 2022 (MSc thesis Proof Complexity with the Help of Sunflowers)
Asger Kjeldsen, University of Copenhagen, 2021 (BSc thesis Applied Presolve Reductions in Pseudo-Boolean Solving)
Johan Lindblad, KTH Royal Institute of Technology, 2018, (MSc thesis On the Structure of Resolution Refutations Generated by Modern CDCL Solvers)
Aleix Sacrest Gascón, Universitat Politècnica de Catalunya, Barcelona, Spain, research intern at KTH Royal Institute of Technology January-June 2017 (BSc thesis Study of Efficient Techniques for Implementing a Pseudo-Boolean Solver Based on Cutting Planes)
Thomas Magnard, École normale supérieure (ENS), Paris, France, research intern at KTH Royal Institute of Technology March-July 2015
Gustav Sennton, KTH Royal Institute of Technology, 2014 (MSc thesis On Conflict Driven Clause Learning — a Comparison Between Theory and Practice with additional files containing all plots and tables)

Group Alumni

Kilian Risse, PhD October 2022 (PhD thesis On Long Proofs of Simple Truths) [advised jointly with Johan Håstad and Per Austrin at KTH Royal Institute of Technology]
Stephan Gocht, PhD June 2022 (PhD thesis Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning)
Jo Devriendt, postdoctoral researcher (2018-2020)
Janne Kokkala, postdoctoral researcher (2018-2020)
Jan Elffers, PhD student (2014-2020)
Dmitry Sokolov, postdoctoral researcher (2017-2020)
Susanna F. de Rezende, PhD June 2019 (PhD thesis Lower Bounds and Trade-offs in Proof Complexity; awarded Stockholm Mathematics Centre Prize for Excellent Doctoral Dissertation 2018/2019)
Guillaume Lagarde, postdoctoral researcher (2018-2019) [hosted jointly with Johan Håstad and Per Austrin]
Meysam Aghighi, postdoctoral researcher (2017-2018)
Sagnik Mukhopadhyay, postdoctoral researcher (2017-2018)
Aaron Potechin, postdoctoral researcher (2017-2018) [hosted jointly with Johan Håstad and Per Austrin]
Ilario Bonacina, postdoctoral researcher 2015-2017
Jesús Giráldez Crú, postdoctoral researcher 2016-2017
Marc Vinyals, PhD June 2017 (PhD thesis Space in Proof Complexity)
Mladen Mikša, PhD January 2017 (PhD thesis On Complexity Measures in Polynomial Calculus)
Christoph Berkholz, postdoctoral researcher February-August 2015
Massimo Lauria, postdoctoral researcher 2012-2015

Long-Term Visitors

(Visitors for one month or more.)

Marc Vinyals, May 2022
Massimo Lauria, Universitat Politècnica de Catalunya, August-October 2016
Alexander Razborov, University of Chicago, March-April 2015
Ilario Bonacina, Sapienza – Università di Roma, January-May 2014
Navid Talebanfard, Aarhus University, January-March 2014
Yuval Filmus, University of Toronto, November-December 2012
Bangsheng Tang, Tsinghua University, January-February 2012
Chris Beck, Princeton University, January-February 2012
Trinh Huynh, University of Washington and ETH Zurich, August-September 2011

Short-Term Visitors

Marcus Anders, Technische Universität Darmstadt, May 2024
Bart Bogaerts, Katholieke Universiteit Leuven, May 2024
Ciaran McCreesh and Matthew McIlree, University of Glasgow, May 2024
Ninad Rajgopal, University of Cambridge, February-March 2024
Kilian Risse, EPFL, January 2024
Justin Pearson, Uppsala University, November 2023
Yogesh Dahiya, Institute of Mathematical Sciences, Chennai, October 2023
Bruno Pasqualotto Cavalar, University of Warwick, October 2023
Leonid Reyzin, Boston University, October 2023
Ciaran McCreesh and Matthew McIlree, University of Glasgow, June 2023
Malte Helmert, University of Basel, May-June 2023
Siddhartha Jain, UT Austin, February 2023
Gioni Mexi, Zuse Institute Berlin, January 2023
Matti Järvisalo, Jeremias Berg, Hannes Ihalainen, and Christoph Jabs, University of Helsinki, December 2022
Kilian Risse, EPFL, November 2022
Emre Yolcu, Carnegie Mellon University, October 2022
Robert Andrews, University of Illinois Urbana-Champaign, October 2022
Marijn Heule, Carnegie Mellon University, June 2022
Allan Sapucaia, University of Campinas, March 2022
Elina Rönnberg, Linköping University, November 2021
Daniela Kaufmann, Johannes Kepler Universität Linz, November 2019
Vincent Liew, University of Washington, November 2019
Susan Margulies, United States Naval Academy, October 2019
Marc Vinyals, Technion – Israel Institute of Technology, October 2019
Anastasia Sofronova, St. Petersburg State University, September-October 2019
Shuo Pang, University of Chicago, September 2019
Daniel Dadush, CWI, August 2019
Amit Chakrabarti, Dartmouth College, June 2019
Kuldeep Meel and Mate Soos, National University of Singapore, May 2019
Ciaran McCreesh, University of Glasgow, April 2019
Paul Beame, University of Washington, March-April 2019
Shiteng Chen, Chinese Academy of Sciences, August 2018
Guillaume Lagarde, Université Paris Diderot, June 2018
Or Meir, University of Haifa, May 2018
Daniela Kaufmann (then Ritirc), Johannes Kepler Universität Linz, April 2018
Avishay Tal, Stanford University, April 2018
Aleksandar Zeljic, Uppsala University March 2018
Janne Kokkala, Aalto University, March 2018
Annie Raymond , University of Massachusetts Amherst, March 2018
Jo Devriendt, Katholieke Universiteit Leuven, March 2018
Thomas Watson, University of Memphis, December 2017
Johannes Klaus Fichte, Technische Universität Wien, November-December 2017
Bart Bogaerts, Katholieke Universiteit Leuven, November 2017
Romain Wallon, Université d'Artois, September 2017
Robert Robere, University of Toronto, May-June 2017
Igor Carboni Oliveira, Charles University, March-April 2017
Aaron Potechin, Institute for Advanced Study, March 2017
Ciaran McCreesh, University of Glasgow, March 2017
Martina Seidl, Johannes Kepler Universität Linz, January 2017
Pavel Pudlák, Institute of Mathematics of the Czech Academy of Sciences, November 2016
Sagnik Mukhopadhyay, Tata Institute of Fundamental Research, Mumbai, October 2016
Joël Alwen, Institute of Science and Technology Austria, April 2016
Laurent Simon, Université de Bordeaux, April 2016
Florent Capelli, Université Paris Diderot, March 2016
Priyank Kalla, University of Utah, March 2016
Karem Sakallah, University of Michigan and Qatar Computing Research Institute, March 2016
Kristin Yvonne Rozier, University of Cincinnati, December 2015
Armin Biere, Johannes Kepler Universität Linz, December 2015
Li-Yang Tan, Toyota Technological Institute at Chicago, October 2015
Jesús Giráldez Crú, Artificial Intelligence Research Institute (IIIA-CSIC), Barcelona, May 2015
Thore Husfeldt, Lund University and IT University of Copenhagen, May 2015
Ilario Bonacina, Sapienza – Università di Roma, April 2015
Michael Forbes, Simons Institute for the Theory of Computing at UC Berkeley, November 2014
Marijn Heule, University of Texas at Austin, October 2014
Benjamin Rossman, National Institute of Informatics, Tokyo, June 2014
Janne H. Korhonen, University of Helsinki, April 2014
Igor Shinkar, Weizmann Institute of Science, April 2014
Prahladh Harsha, Tata Institute of Fundamental Research, Mumbai, March 2014
Jan Johannsen, Ludwig-Maximilians-Universität München, March 2014
Siu Man Chan, Princeton University, December 2013
Daniel Le Berre, Université d'Artois, November 2013
Klas Markström, Umeå University, November 2013
Albert Atserias, Universitat Politècnica de Catalunya, August 2013
Christoph Berkholz, RWTH Aachen University, April 2013
Dominik Scheder, Aarhus University, February 2013
Nicola Galesi and Ilario Bonacina, Sapienza – Università di Roma, February 2013
Alexander Dreyer and Thanh Hung Nguyen, Fraunhofer Institute for Industrial Mathematics ITWM, November 2012
Troy Lee, Centre for Quantum Technologies, October 2012
Joshua Brody, Aarhus University, September 2012
Rustan Leino, Microsoft Research Redmond, March 2012.
Matti Järvisalo, University of Helsinki, December 2011
Noga Ron-Zewi, Technion – Israel Institute of Technology, December 2011
Arkadev Chattopadhyay, University of Toronto, September 2011
Rahul Santhanam, University of Edinburgh, September 2011
Arie Matsliah, IBM Research Haifa and Technion – Israel Institute of Technology, August 2011
Stanislav Živný , University of Oxford, May 2011
Iddo Tzameret, Tsinghua University, May 2011

Funding

Our research have at different stages been generously funded by

a Junior Researcher Position Grant from the Swedish Research Council,
a Starting Independent Researcher Grant from the European Research Council,
a Breakthrough Research Grant from the Swedish Research Council,
a Grant for Research Projects with High Scientific Potential from the Knut and Alice Wallenberg Foundation (co-PI),
a Consolidator Grant from the Swedish Research Council,
a Postdoctoral Scholarship Program in Mathematics Grant from the Knut and Alice Wallenberg Foundation,
a Research project 2 grant from the Independent Research Fund Denmark,
an academic doctoral student grant from the Wallenberg AI, Autonomous Systems and Software Program (WASP).

Workshops

Workshops, seminar weeks, et cetera co-organized by Jakob Nordström:

NordConsNet 2023, the annual workshop for the Nordic network for researchers and practitioners of constraint programming, Odense, Denmark, June 8-9, 2023.
Extended reunion of the program Satisfiability: Theory, Practice, and Beyond, Simons Institute for the Theory of Computing at UC Berkeley, March-May 2023.
Theory and Practice of SAT and Combinatorial Solving, Schloss Dagstuhl – Leibniz Center for Informatics, October 10-14, 2022.
Satisfiability: Theory, Practice, and Beyond, semester program at the Simons Institute for the Theory of Computing at UC Berkeley, January-May 2021. [Converted to virtual format due to the Covid-19 pandemic.]
Proof Complexity, Banff International Research Station, January 19-24, 2020 (see video of all presentations).
6th Swedish Summer School in Computer Science, June 30 – July 6, 2019, with lectures by Madhu Sudan and Luca Trevisan.
Theory and Practice of Satisfiability Solving, Casa Matemática Oaxaca (affiliated with BIRS), August 26-31, 2018 (see video of all presentations).
5th Swedish Summer School in Computer Science (S³CS 2018), August 5-11, 2018, with lectures by Ronald de Wolf and Oded Regev.
Proof complexity, Schloss Dagstuhl – Leibniz Center for Informatics, January 28 – February 2, 2018 (see workshop report).
Proof Complexity and Beyond, Mathematisches Forschungsinstitut Oberwolfach, August 13-19, 2017 (see workshop report).
4th Swedish Summer School in Computer Science (S³CS 2017), July 16-22, 2017, with lectures by Benjamin Rossman and Ryan Williams.
Theoretical Foundations of SAT Solving, Fields Institute, Toronto, August 15-19, 2016.
3rd Swedish Summer School in Computer Science (S³CS 2016), June 26 – July 2, 2016, with lectures by Michael Mitzenmacher and Sergei Vassilvitskii.
2nd Swedish Summer School in Computer Science (S³CS 2015), June 28 – July 4, 2015, with lectures by Venkatesan Guruswami and Sergey Yekhanin.
Theory and Practice of SAT Solving, Schloss Dagstuhl – Leibniz Center for Informatics, April 19-24, 2015 (see workshop report).
Swedish Summer School in Computer Science (S³CS 2014), June 29 – July 5, 2014, with lectures by Boaz Barak and Ryan O'Donnell.
Theoretical Foundations of Applied SAT Solving, Banff International Research Station, January 19-24, 2014 (see video of all presentations, the workshop report, and a Communications of the ACM editorial about the workshop).

Publications

Below follows a list of publications, sorted in reverse chronological order, emanating from the MIAO research group. As a general rule, these papers are copyright by their respective publishers but are free for personal use.

Please note that the list below is updated at somewhat irregular intervals. The last proper update was in September 2023. See www.jakobnordstrom.se/publications for a full list of Jakob Nordström's publications (which is updated more frequently, but does not contain papers by other members of the group on which Jakob Nordström is not a co-author).

2023

Jonas Conneryd, Susanna F. de Rezende, Jakob Nordström, Shuo Pang, and Kilian Risse. Graph Colouring Is Hard on Average for Polynomial Calculus and Nullstellensatz. To appear in Proceedings of the 64th Annual IEEE Symposium on Foundations of Computer Science (FOCS '23).
Gioni Mexi, Timo Berthold, Ambros Gleixner, and Jakob Nordström. Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. In Proceedings of the 29th International Conference on Principles and Practice of Constraint Programming (CP '23), Leibniz International Proceedings in Informatics (LIPIcs), volume 280, pages 27:1-27:19, August 2023.
Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract). Best Papers from Sister Conferences Track in the Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI '23), pages 6436-6441, August 2023.
Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified Symmetry and Dominance Breaking for Combinatorial Optimisation. Journal of Artificial Intelligence Research, volume 77, pages 1539-1589, August 2023.
Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified Core-Guided MaxSAT Solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE-29), Lecture Notes in Computer Science, volume 14132, pages 1-22, July 2023.

2022

Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An Auditable Constraint Programming Solver. In Proceedings of the 28th International Conference on Principles and Practice of Constraint Programming (CP '22), Leibniz International Proceedings in Informatics (LIPIcs), volume 235, pages 25:1-25:18, August 2022.
Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel. Certified CNF Translations for Pseudo-Boolean Solving. In Proceedings of the 25th International Conference on Theory and Applications of Satisfiability Testing (SAT '22), Leibniz International Proceedings in Informatics (LIPIcs), volume 236, pages 16:1-16:25, August 2022. SAT '22 best paper award.
Daniela Kaufmann, Paul Beame, Armin Biere and Jakob Nordström. Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. In Proceedings of the 25th Design, Automation and Test in Europe Conference (DATE '22), pages 1435-1440, March 2022.
Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified Symmetry and Dominance Breaking for Combinatorial Optimisation. In Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI '22), pages 3698-3707, February 2022. AAAI '22 distinguished paper award.

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: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.
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.
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.
Susanna F. de Rezende, Or Meir, Jakob Nordström, and Robert Robere. Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. Computational Complexity, volume 30, issue 1, pages 4:1-4:45, June 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.

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. 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.)
Jo Devriendt. Watched Propagation of 0-1 Integer Linear Constraints. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), Lecture Notes in Computer Science, volume 12333, pages 160-176, September 2020.
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.
Mate Soos, Stephan Gocht, and Kuldeep S. Meel. Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling. In Proceedings of the 32nd International Conference on Computer Aided Verification (CAV '20), Part I, Lecture Notes in Computer Science, volume 12224, pages 463-484, July 2020.
Dmitry Sokolov. (Semi)Algebraic Proofs over {±1}Variables. In Proceedings of the 52nd Annual ACM Symposium on Theory of Computing (STOC '20), pages 78-90, June 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.
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), Leibniz International Proceedings in Informatics (LIPIcs), volume 151, pages 72:1-72:16, January 2020.

2019

Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich. Using Relational Verification for Program Slicing. In Proceedings of the 17th International Conference on Software Engineering and Formal Methods (SEFM '19), Lecture Notes in Computer Science, volume 11724, pages 353-372, September 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.
Tu-San Pham, Jo Devriendt, and Patrick De Causmaecker. Declarative Local Search for Predicate Logic. In Proceedings of the 15th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR '19), pages 340-346, June 2019.
Marjolein Deryck, Joost Vennekens, Jo Devriendt, and Simon Marynissen. Legislation in the Knowledge Base Paradigm: Interactive Decision Enactment for Registration Duties. In Proceedings of the 13th International Conference on Semantic Computing (ICSC '19), pages 174-177, January-February 2019.
Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in Monotone Complexity and TFNP. In Proceedings of the 10th Innovations in Theoretical Computer Science Conference (ITCS '19), Leibniz International Proceedings in Informatics (LIPIcs), volume 124, pages 38:1-38:19, January 2019.

2018

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.
Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. In Proceedings of the 50th Annual ACM Symposium on Theory of Computing (STOC '18), pages 902-911, June 2018.
Arkadev Chattopadhyay, Michal Koucký, Bruno Loff, and Sagnik Mukhopadhyay. Simulation Beats Richness: New Data-Structure Lower Bounds. In Proceedings of the 50th Annual ACM Symposium on Theory of Computing (STOC '18), pages 1013-1020, June 2018.
Sam Buss, Dmitry Itsykson, Alexander Knop, and Dmitry Sokolov. Reordering Rule Makes OBDD Proof Systems Stronger. In Proceedings of the 33rd Annual Computational Complexity Conference (CCC '17), Leibniz International Proceedings in Informatics (LIPIcs), volume 102, pages 16:1-16:24, June 2018.

2017

Ilario Bonacina. Space in Weak Propositional Proof Systems. Springer, 2017.
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.
Ilario Bonacina and Navid Talebanfard. Strong ETH and Resolution via Games and the Multiplicity of Strategies. Algorithmica, volume 79, issue 1, pages 29-41, September 2017.
Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, and Jordi Levy. Structure Features for SAT Instances Classification Journal of Applied Logic, volume 23, pages 27-39, September 2017.
Jesús Giráldez-Cru and Jordi Levy. Locality in Random SAT Instances. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI '17), pages 638-644, August 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.
Guillaume Baud-Berthier, Jesús Giráldez-Cru, and Laurent Simon. On the Community Structure of Bounded Model Checking SAT Problems. In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT '17), Lecture Notes in Computer Science, volume 10491, pages 65-82, August 2017.
Patrick Bennett, Ilario Bonacina, Nicola Galesi, Tony Huynh, Mike Molloy, and Paul Wollan. Space proof complexity for random 3-CNFs. Information and Computation, volume 255, part 1, pages 165-176, 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.
Massimo Lauria, Pavel Pudlák, Vojtěch Rödl and Neil Thapen. The Complexity of Proving That a Graph Is Ramsey. Combinatorica, volume 37, issue 2, pages 253-268, April 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.

2016

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.
Ilario Bonacina, Nicola Galesi, and Neil Thapen. Total Space in Resolution. SIAM Journal on Computing, volume 45, issue 5, pages 1894-1909, 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.
Ilario Bonacina. Total Space in Resolution Is at Least Width Squared. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP '16), Leibniz International Proceedings in Informatics (LIPIcs), volume 55, pages 56:1-56:13, 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.
Massimo Lauria. A Rank Lower Bound for Cutting Planes Proofs of Ramsey's Theorem. ACM Transactions on Computation Theory, volume 8, issue 4, article 17, June 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.
Yuval Filmus, Pavel Hrubeš, and Massimo Lauria. Semantic Versus Syntactic Cutting Planes. In Proceedings of the 33rd Symposium on Theoretical Aspects of Computer Science (STACS '16), pages 35:1-35:13, February 2016.
Ilario Bonacina and Navid Talebanfard. Improving Resolution Width Lower Bounds for k-CNFs with Applications to the Strong Exponential Time Hypothesis. Information Processing Letters, volume 116, issue 2, pages 120-124, February 2016.
Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower Bounds: From Circuits to QBF Proof Systems. In Proceedings of the 7th Innovations in Theoretical Computer Science Conference (ITCS '16), pages 249-260, January 2016.

2015

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.
Ilario Bonacina and Navid Talebanfard. Strong ETH and Resolution via Games and the Multiplicity of Strategies. In Proceedings of the 10th International Symposium on Parameterized and Exact Computation (IPEC '15), Leibniz International Proceedings in Informatics (LIPIcs), volume 43, pages 248-257, September 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.
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.)
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.

2014

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.
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.

2013

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.
Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A Characterization of Tree-Like Resolution Size. In Information Processing Letters, volume 113, number 18, pages 666-671, September 2013.
Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Parameterized Complexity of DPLL Search Procedures In ACM Transactions on Computational Logic, volume 14, issue 3, article 23, August 2013.
Massimo Lauria. A Rank Lower Bound for Cutting Planes Proofs of Ramsey Theorem. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13), pages 351-364, July 2013.
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.
Massimo Lauria, Pavel Pudlak, Vojtěch Rödl, and Neil Thapen. The Complexity of Proving That a Graph Is Ramsey. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP '13), Lecture Notes in Computer Science, volume 7965, pages 684-695, 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.

2012

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. Space Complexity in Polynomial Calculus. Technical Report TR12-132, Electronic Colloquium on Computational Complexity (ECCC), October 2012.
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), pages 316-331, October 2012.
Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A. Razborov. Parameterized Bounded-depth Frege Is Not Optimal. In ACM Transaction on Computational Theory, volume 4, issue 3, article 7, September 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.

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.