Category Archives: my_research

Quality of Life Improvements to Loandra

Leave a reply

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.

Back From FloC

Leave a reply

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

1 Reply

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.

Camera Ready Papers Available

Leave a reply

The four papers accepted at Floc 2022 are now available from my publications page:

If you want to discuss any of these in more detail, let me know and I’d be happy to.
Once again, thanks to all my co-authors!

New Papers Accepted

Leave a reply

I am pleased to let you know that my spring season of research ended with 4 papers accepted at FLoC 2022.
Three at the SAT conference:

  • MaxSAT-Based Bi-Objective Boolean Optimization with Christoph Jabs, Andreas Niskanen and Matti Jävisalo.
    • The paper describes a SAT-based approach for computing the pareto-front of biobjective optimization problems.
  • Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization with Pavel Smirnov and Matti Järvisalo
    • The paper describes improvements to the implicit hitting set algorithm for pseudo-Boolean optimization that we proposed in last years CP conference.
  • Incremental Maximum Satisfiability with Andreas Niskanen and Matti Järvisalo
    • The paper describes an API for implementing incremental Maximum Satisfiability as well as a solver that implements it.

And the paper Clause Redundancy and Preprocessing in Maximum Satisfiability with Hannes Ihalainen and Matti Järvisalo at the IJCAR conference.

All of the papers will be available after the camera ready deadlines have passed. Let me know if you want to get a copy of them beforehand.

I’d like to thank all of my coauthors. See you at Haifa in August.

Good performance at the MSE2021

Leave a reply

The results of the 2021 MaxSAT Evaluation were just announced at the 2021 SAT conference (by me :)). My solver Loandra performed very well, taking first place in the weighted 300s track and fourth in all other tracks. The source code of that version of Loandra is already available at the evaluation website and in its repository.


I would like to thank my co-organizers of the Evaluation and the organizers of the SAT conference. I am looking forward to taking a closer look at the results.

The spring of presentations continues

Leave a reply

A week ago I gave the second talk at the Simons Institute, this time at the Theoretical Foundations of SAT/SMT Solving seminar. The event webpage can be found here. I had the opportunity to talk about my work on preprocessing for Maximum Satisfiability, covering work done both during and after the preprocessing.

I would again like to thank Marjin Heule for considering me as a speaker for the event. Next time you can hear me speak is at Jakob Nordströms video seminars on the 4.6. I will talk about Abstract Cores in the IHS algorithm for MaxSAT, covering my recent paper from SAT 2020. Looking forward to seeing you there!

Invited Talks at the Simons Institute

Leave a reply

This spring I have been very fortunate to have been invited to give to talks at the various different seminars run by the Simons Institute in California.

The first talk on solving MaxSAT was given on the 13th of April together with Matti Järvisalo. The talk was a part of the Beyond Satisfiability seminar, a recording of it can be found here.

The second talk will be on MaxSAT preprocessing on May 5th as a part of the Theoretical Foundation of SAT/SMT solving workshop. More information can be found here. As the talk is online. I invite anyone who is interested to attend. I am sure the talks will be interesting, personally I am looking forward to hearing about SAT and QBF preprocessing form Benjamin and Martina.

I would like to thank the organisers of the various seminars of the Simons Institute for considering me as a speaker in their events.

My Thesis won an Award

Leave a reply

I am happy to let you know that my Thesis: Solving Optimization Problems via Maximum Satisfiability: Encodings and Re-Encodings was awarded the international ACP Doctoral Thesis Award by the Association of Constraint Programming. I will be receiving the award and giving a presentation on my thesis on the 11.9 at the CP 2020 conference. The conference is virtual and free to attend, I hope to see you all there.

Im an honoured for receiving the price and want to thank the ACP for the recognition.
My presentation can be found at: at google drive.

A news article with more info can be found at: https://www.helsinki.fi/en/news/data-science-news/international-dissertation-award-to-berg

Best Paper award at SAT 2020

Leave a reply

bpaper-page001

I am happy to let you know that my paper titled Abstract Cores in Implicit Hitting set MaxSat solving has been awarded a best paper award at the 2020 SAT conference. The paper reports on work that was started during my visit to Toronto in 2019. We propose a technique that seeks to address the inherent drawback in the so called implicit hitting set approach to MaxSAT solving, one of the most successful approaches to solving MaxSAT instances corresponding to real world applications. Abstract cores seek to reduce the number of cores that the algorithm needs to extract before terminating without increasing the complexity of the core extraction steps too much. The instantiation of this idea in the MaxHS solver was one of the best performing approaches in the 2020 MaxSAT Evaluation.

I would like to thank the conference organizers for the recognition and for putting together an event that, considering the current circumstances, was probably the best possible way of organizing SAT 2020. I would also like to thank my co-authors, especially Prof. Fahiem Bacchus for his efforts in the implementation and getting the experimental results.