Mathematical Insights into Algorithms for Optimization (MIAO) Group
Latest News

We need to hire both PhD students and postdocs to rebuild
the research group after the move to Copenhagen and Lund!
Please check out the
open positions webpage
for news about current and/or upcoming openings!

A team including MIAO member Stephan Gocht placed second in the
Fixed CNF Encoding Race of the
EDA Challenge 2021.
Congratulations, Stephan!

That 2020 has been a thrilling year is somewhat of an
understatement, but for the MIAO group the first academic year at
the University of Copenhagen and Lund University has been filled
with excitement for all the right reasons!
Our works on designing stateoftheart algorithms for combinatorial
optimization problems, and making sure not only that such algorithms
run fast but that we also understand how they perform and can prove
that they produce correct results, have appeared in the premier AI
conferences AAAI and IJCAI (3 papers), as well as
in more specialized highprofile conferences on combinatorial
optimization such as CP, CPAIOR, and SAT
(6 papers), and on formal verification such as CAV
and FMCAD (2 papers). On the flip side, research
contributions focusing on understanding the limitations of such
optimization algorithms, or of efficient computation in general,
from a rigorous, mathematical point of view have been accepted to
top theoretical computer science conferences such
as STOC, FOCS, CCC, and ITCS
(5 papers).
After this veritable explosion of 16 conference papers during 2020
(not counting journal papers and technical reports), we are not
quite sure what to expect going forward, but so far it sure seems
like the MIAO kitten is indeed enjoying life in the company of the
big, friendly BARC dog…
Briefly 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
(where we are friendly neighbours with
BARC).
The MIAO research group has a unique profile in that we are doing
cuttingedge research both on the mathematical foundations of
efficient computation and on stateoftheart practical algorithms
for realworld problems.
This creates a very special environment, where we do not only conduct
indepth research on different theoretical and applied topics, but
where different lines of research crossfertilise 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.
On the practical side, we want to gain a more rigorous scientific
understanding, and improve the performance, of modern algorithms for
automated reasoning and combinatorial optimization.
We are particularly interested in harnessing powerful mathematical
tools such as Gröbner bases or 01 integer linear programming (also
known as pseudoBoolean solving) to achieve exponential improvements
in performance, which seems possible in theory but has so far been
hard to achieve in practice.
Our most active line of work right now is focusing on
combining ideas from SAT solving and mixed integer linear
programming (MIP) to construct a new 01 integer linear programming
solver
RoundingSat.
This solver is already worldleading when it comes to pseudoBoolean solving,
but our goal is to develop it further, integrating ideas also from
MaxSAT solving, MIP solving, satisfiability modulo theories (SMT)
solving, and constraint programming (CP), ultimately hoping to go
significantly beyond the current state of the art.
Quite recently, we have also begun making investigations into, and
have had some research breakthrough on,
how to verify the correctness of stateoftheart algorithms for combinatorial
optimization. Such algorithms are often highly complex, and even
mature commercial solvers are known to sometimes produce wrong
results. What we are working on is to enhance the currently best
combinatorial solvers to make them certifying, i.e., so that
they output not only a solution but also a simple, machineverifiable
proof that the claimed solution is correct and complete—this is also
known as proof logging.
For such a certifying solver, the workflow becomes as follows:

Run the solver on a problem instance to obtain not only a
solution, but also a proof of correctness.

Feed the problem, the solution, and the proof to a special,
dedicated proof checker for verification.

Accept the solution if the proof checker says that the proof is valid.
Importantly, these machineverifiable 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.
Our research in this area is still very much work in progress, but
our tool
VeriPB
can already provide efficient proof logging for some
solving techniques that have long remained beyond the reach of other tools.
Principal Investigator
Jakob Nordström
Researchers
We are currently actively hiring to rebuild the research group
after the move to Copenhagen and Lund, so stay tuned…
BSc and MSc Students

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
JanuaryJune 2017
(BSc thesis
Study of Efficient Techniques for
Implementing a PseudoBoolean Solver Based on Cutting Planes)

Thomas Magnard, École normale supérieure (ENS), Paris, France,
research intern
at KTH Royal Institute of Technology
MarchJuly 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

Jo Devriendt,
postdoctoral researcher (20182020)

Janne Kokkala,
postdoctoral researcher (20182020)

Jan Elffers,
PhD student (20142020)

Dmitry Sokolov,
postdoctoral researcher (20172020)

Susanna
F. de Rezende,
PhD June 2019
(PhD thesis
Lower Bounds and Tradeoffs
in Proof Complexity;
awarded
Stockholm Mathematics
Centre Prize for Excellent Doctoral Dissertation 2018/2019)

Guillaume Lagarde,
postdoctoral researcher (20182019)
[hosted jointly with
Johan Håstad
and
Per Austrin]

Meysam Aghighi,
postdoctoral researcher (20172018)

Sagnik Mukhopadhyay,
postdoctoral researcher (20172018)

Aaron Potechin,
postdoctoral researcher (20172018)
[hosted jointly with
Johan Håstad
and
Per Austrin]

Ilario Bonacina,
postdoctoral researcher 20152017

Jesús Giráldez Crú,
postdoctoral researcher 20162017

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 FebruaryAugust 2015

Massimo Lauria,
postdoctoral researcher 20122015
LongTerm Visitors
(Visitors for one month or more.)

Massimo Lauria,
Universitat Politècnica de Catalunya,
AugustOctober 2016

Alexander Razborov,
University of Chicago,
MarchApril 2015

Ilario Bonacina,
Sapienza – Università di Roma,
JanuaryMay 2014

Navid Talebanfard,
Aarhus University, JanuaryMarch 2014

Yuval Filmus,
University of Toronto,
NovemberDecember 2012

Bangsheng Tang,
Tsinghua University,
JanuaryFebruary 2012

Chris Beck,
Princeton University,
JanuaryFebruary 2012

Trinh Huynh,
University of Washington and ETH Zurich,
AugustSeptember 2011
ShortTerm Visitors
(Visitors since August 2019 received in Copenhagen and/or Lund.
All planned visits since early 2020 have been cancelled due to
the Covid19 pandemic. We are eagerly waiting for conditions to
change so that our vibrant exchange of visitors can resume.)

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,
SeptemberOctober 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,
MarchApril 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,
NovemberDecember 2017

Bart Bogaerts,
Katholieke Universiteit Leuven,
November 2017

Romain Wallon,
Université d'Artois,
September 2017

Robert Robere,
University of Toronto,
MayJune 2017

Igor Carboni Oliveira,
Charles University,
MarchApril 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

LiYang Tan,
Toyota Technological Institute at Chicago,
October 2015

Jesús Giráldez Crú,
Artificial Intelligence Research Institute
(IIIACSIC), 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,
LudwigMaximiliansUniversitä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 RonZewi,
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 (coPI),

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.
Workshops
Workshops, seminar weeks, et cetera coorganized by Jakob
Nordström:

Theory
and Practice of SAT and Combinatorial Solving,
Schloss Dagstuhl – Leibniz Center for Informatics,
October 1014, 2022.
[Rescheduled from September 2020 due to the Covid19 pandemic.]

Satisfiability:
Theory, Practice, and Beyond,
semester program at the Simons Institute for the Theory of
Computing at UC Berkeley, JanuaryMay 2021.
[Converted to virtual format due to the Covid19 pandemic.]

Proof
Complexity,
Banff International Research Station,
January 1924, 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 2631, 2018
(see
video
of all presentations).

5th Swedish Summer School in
Computer Science (S^{3}CS 2018),
August 511, 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 1319, 2017
(see
workshop
report).

4th Swedish Summer School in
Computer Science (S^{3}CS 2017),
July 1622, 2017,
with lectures by
Benjamin Rossman
and
Ryan Williams.

Theoretical Foundations of SAT Solving,
Fields Institute, Toronto, August 1519, 2016.

3rd Swedish Summer School in
Computer Science (S^{3}CS 2016),
June 26 – July 2, 2016,
with lectures by
Michael Mitzenmacher
and
Sergei Vassilvitskii.

2nd Swedish Summer School in
Computer Science (S^{3}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 1924, 2015
(see
workshop report).

Swedish Summer School in
Computer Science (S^{3}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 1924, 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 March 2021.
See
www.csc.kth.se/~jakobn/research/
for a full list of Jakob Nordström's publications
(which is updated much more frequently, but does not contain papers by other
members of the group on which Jakob Nordström is not a coauthor).
2021

Susanna F. de Rezende, Mika Göös, Jakob Nordström,
Toniann Pitassi, Robert Robere, and Dmitry Sokolov.
Automating Algebraic Proof Systems is NPHard.
To appear in
Proceedings of the 53rd Annual ACM Symposium on Theory of Computing
(STOC '21),
June 2021.

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

Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria,
Jakob Nordström, and Alexander Razborov.
Clique Is Hard on Average for Regular Resolution.
To appear in
Journal of the ACM, 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.
To appear in
Proceedings of the
35th AAAI Conference on Artificial Intelligence (AAAI '21),
February 2021.

Stephan Gocht and Jakob Nordström.
Certifying Parity Reasoning Efficiently Using PseudoBoolean Proofs.
To appear in
Proceedings of the
35th AAAI Conference on Artificial Intelligence (AAAI '21),
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 233350. IOS Press, 2021.

Susanna F. de Rezende, Or Meir, Jakob Nordström, and Robert Robere.
Nullstellensatz SizeDegree Tradeoffs from Reversible Pebbling.
Computational Complexity,
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.
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 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.)

Jo Devriendt.
Watched Propagation of 01 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 160176, 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 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.

Mate Soos, Stephan Gocht, and Kuldeep S. Meel.
Tinted, Detached, and Lazy CNFXOR 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 463484,
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 7890, 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 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.

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),
Leibniz International Proceedings in Informatics (LIPIcs),
volume 151, pages 72:172: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 353372,
September 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.

TuSan 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 340346, 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 174177, JanuaryFebruary 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:138:19,
January 2019.
2018

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.

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 902911, June 2018.

Arkadev Chattopadhyay, Michal Koucký, Bruno Loff, and Sagnik Mukhopadhyay.
Simulation Beats Richness: New DataStructure Lower Bounds.
In
Proceedings of the 50th Annual ACM Symposium on Theory of Computing
(STOC '18),
pages 10131020, 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:116:24, June 2018.
2017

Ilario Bonacina.
Space in Weak Propositional Proof Systems.
Springer, 2017.

Massimo Lauria and Jakob Nordström.
Tight SizeDegree Bounds for SumsofSquares Proofs.
Computational Complexity,
volume 26, issue 3, pages 911948, December 2017.

Ilario Bonacina and Navid Talebanfard.
Strong ETH and Resolution via Games and the Multiplicity of Strategies.
Algorithmica,
volume 79, issue 1, pages 2941, September 2017.

Carlos Ansótegui, Maria Luisa Bonet, Jesús GiráldezCru, and Jordi Levy.
Structure Features for SAT Instances Classification
Journal of Applied Logic,
volume 23, pages 2739, September 2017.

Jesús GiráldezCru and Jordi Levy.
Locality in Random SAT Instances.
In
Proceedings of the 26th International Joint Conference on
Artificial Intelligence (IJCAI '17),
pages 638644, 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 464473, August 2017.

Guillaume BaudBerthier, Jesús GiráldezCru, 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 6582, August 2017.

Patrick Bennett, Ilario Bonacina, Nicola Galesi,
Tony Huynh, Mike Molloy, and Paul Wollan.
Space proof complexity for random 3CNFs.
Information and Computation,
volume 255, part 1, pages 165176, 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.

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 253268,
April 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.
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 295304, October 2016.

Ilario Bonacina, Nicola Galesi, and Neil Thapen.
Total Space in Resolution.
SIAM Journal on Computing,
volume 45, issue 5, pages 18941909, 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.

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:156:13, 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.

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:135:13, February 2016.

Ilario Bonacina and Navid Talebanfard.
Improving Resolution Width Lower Bounds for kCNFs with Applications to the
Strong Exponential Time Hypothesis.
Information Processing Letters,
volume 116, issue 2, pages 120124, 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 249260, 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 466485,
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 248257, September 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.

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

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.
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 16, 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 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.
2013

Jakob Nordström.
Pebble Games, Proof Complexity, and TimeSpace Tradeoffs.
Logical Methods in Computer Science,
volume 9, issue 3, article 15, September 2013.

Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A Characterization
of TreeLike Resolution Size. In Information Processing Letters,
volume 113, number 18,
pages 666671, 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 351364, 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 437448, 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 684695, 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.
2012

Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga RonZewi, and Neil Thapen.
Space Complexity in Polynomial Calculus.
Technical Report TR12132,
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 316331, October 2012.

Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A.
Razborov. Parameterized Boundeddepth 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 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.
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.
