Author Archives: Jeremias

About Jeremias

I am a soon-to-be doctor of computer science from the University of Helsinki. My main research interests are NP-hard optimization problems and in particular constraint optimization. I am also interested in several areas of operations research and data analysis in general.

Quality of Life Improvements to Loandra

As a consequence of someone pointing out a bug in my MaxSAT solver Loandra I have today finally brought the public repository of it up to date. I also learned how to link external libraries properly and how to add submodules to github repositories.

If you do not know, Loandra is an anytime MaxSAT solver. While it can find provably optimal solutions, it is more geared toward finding low-cost solutions quickly. Loandra was created during my visit to Australia in 2018, it implements the so called core-boosted linear search algorithm that—informally speaking—first performs lower bounding search and then upper bounding search on the reformulated objective. Crucial to Loandras performance is also the preprocessing performed by the MaxPRE2 preprocessor.

Long story short, now is a good time to try Loandra if you still have not.
Head over to https://github.com/jezberg/loandra and let me know if (or let’s be honest… when) you find any issues.

New Paper at CADE and IJCAI

I am pleased to announce the acceptance of two new papers at the CADE and IJCAI. The CADE paper is titled Certified Core-Guided MaxSAT Solving and written together with
Bart Bogaerts, Jakob Nordström, Andy Oertel and Dieter Vandesande from Vrije Universiteit Brussel, University of Copenhagen and Lund University. It presents the first approach to proof logging core-guided MaxSAT solving, thus increasing the certainty of the correctness of the results computed by MaxSAT solvers.

The IJCAI paper is titled Unifying Core-Guided and Implicit Hitting Set based Optimization and written together with Hannes Ihalainen, and Matti Järvisalo from the University of Helsinki. It presents an abstract framework that aims to unify core-guided and IHS-based MaxSAT solving.

I’d be happy to discuss either paper in more detail with anyone who is interested. Once the camera ready versions are published I will upload a version to these pages as well.
My sincerest gratitude goes to all of my co-authors, it has been a pleasure working with all of you.

Back from Berkeley

Last week I got back to Helsinki from Berkeley in California, where I had the honor of being invited to the extended reunion of the satisfiability workshop hosted by the Simons Institute of UCB Berkeley. The program consisted of 7 weeks of hanging out with international colleagues, talking science and making the world a slightly better place to live. I was super inspired by all the smart people I met and talked to and am looking forward to seeing what comes out of the multitutde of ideas we discussed.

During my time there I gave a talk at a workshop, a recording of which can be found below.

The while trip would not have been nearly as fun without my partner in crime & life Chride joining me, giving me a nice excuse to also do some sightseeing outside of Berkeley. We visited Yosemite, Big Sur, and the Muir Woods. All amazing places to see.

I’d like to express my sincerest gratitutde toward the SImons Institute, as well as the organizers of the workshop: Jakob Nordström, Albert Atserias, Sam Buss, Vijay Ganesh and Antonina Kolokolova. I had a great and very inspiring time.

Explaining the internals of a computer to 9-year olds

About a week ago I organized a workshop on the internals of a computer as part of the UniJunior project that i have been involved with for a couple of years now. While this was not the first workshop I have been responsible for, it was the first one for which I had created most of the content on my own—which made it that much more nerve-wracking. Luckily the coordinator for UniJunior and the assistants we hired for the workshop were really great (as always).

The 3 hour long workshop was divided into two parts. The first part was spent discussing what a computer is, the kids had a number of differing opinions on that front (can a playstation be considered to be a computer? How bout a tractor?). Afterwards we then opened up a desktop computer, a laptop and an iPhone and looked at which parts they contain.

After a light snack, the second half of the workshop was spent on an exercise designed to simulate the cycle that a processor of a computer performs. Those of you who know Swedish can read detailed instructions on https://docs.google.com/document/d/1eEKHQp8yQH1uVB1RnPcxvytkG1LHk2vrMrxIzgBZeCY/edit#heading=h.phn88zt1pli9 .

While the overall opinion of the task was positive, it did suffer a bit from the fact that most parts of the processor spend most of their time doing nothing :). Luckily the tables on the mother card could be drawn on.

I would like to express my sincerest gratitude to everyone who helped with the workshop! Hopefully we will get the opportunity to do it again in the fall. If you have a Swedish-speaking child of ages 6-9 or know of someone who does, I strongly recommend the UniJunior workshops. All of them are well organized, fun, and inspiring!

Dagstuhl workshop 22411 “Theory and Practice of SAT and Combinatorial Solving”

About a week ago I attended the Dagstuhl workshop 22411 “Theory and Practice of SAT and Combinatorial Solving”. Dagstuhl workshops are one-week events that gather researchers in some topic from across the world to Schloss Dagstuhl – Leibniz-Zentrum für Informatik for a week of presentations on ongoing work and networking. Compared to most conferences, the topics on the workshop are more focused and the atmosphere more relaxed, facilitating more inspiring discussions.

I would like to thank the organisers of the workshop for inviting me. I had a great and inspiring time. Hopefully, the connections made and discussions had will lead to a lot of interesting research in the future!

See you in June of 2023 for the next workshop!

The workshop was held in a castle

New Paper

Our paper: Computing Smallest MUSes of Quantified Boolean Formulas is now available on the webpage. This week Andreas is presenting it at the 16th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR) held in Genova Nervi, Italy.

The paper presents an algorithm for computing smallest unsatisfiable subsets (i.e. sources of inconsistency) of quantified Boolean formulas. Additionally, the paper proves that the complexity of doing so is sigma k+1 p complete for k quantifier blocks (i.e. very difficult, even for computers). The implementation of the algorithm used in our experiments is available on bitbucket. If you want to chat more about the topic, feel free to get in touch!

Thanks to all of my co-authors, Andreas, Jere and Matti.

New Position and Title

I am happy to let you know that tomorrow (on the 1.9.2022) I will start in a new position as a University Lecturer at the Department of Computer Science of the University of Helsinki. In practice this will (hopefully) mean that I will get the opportunity to teach some more in the future.

For a related (but separate) piece of news I have also recently been awarded the title of Docent of Computer Science from the University of Helsinki. Docent is a title that is a bit tricky to translate to English as it tends to have slightly different meanings in different countries. In Finland, it refers to someone with the right to teach their own subject at the University without having to be associated with the University (although often is).

I am grateful and honoured for both the position and the title. Thanks to the department of computer science and the University of Helsinki!

Back From FloC

After about two years of remote conferences I travelled last week to Haifa in Israel to attend the 8th federated logic conference (FLoC 2022) The trip consisted of meeting colleagues, hearing about their exiting research, and getting inspire. In the free time we explored the (very hilly) city of Haifa. The highlight of my trip was giving an invited talk at the SAT conference. I wrote about that in this blogpost.

I’d like to thank the organisers of FloC, as well as the organisers of the SAT conference. See you in 4 years!

Invited Talk at the SAT 2022 conference

Yesterday, on the 4th of August I gave an invited talk on Maximum Satisfiability at the “25 years of SAT” celebratory session of the 2022 SAT conference at Haifa in Israel. Mine was one of 5 talks, the others were given by Alexander Nadel, Armin Biere, Olaf Beyersdorff and Marijn Heule.

I would like to thank the session organiser, Prof. Jakob Nordström for the invite. I had a great time an am very honoured to have been considered together with such established researchers.

Research Visit To Brussels and Delft

In may this year I visited Prof. Bart Bogaerts at the Vrije Universiteit Brussel.. During the two week visit we talked about possible connections between our research. We were also joined by Jakob Nordström, his student Andy Oertel, and Ciaran McCreesh.
At the end of the visit, I also spent a day in Delft talking to Emir Demirović.

I’d like to thank Bart for hosting the visit and everyone else for the interesting discussions. I am looking forward to potential further collaboration.