Tag Archives: MaxSAT

New Paper at CADE and IJCAI

Leave a reply

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.

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.

MaxSAT tutorial at ECAI 2020

Leave a reply

Tomorrow (4.9.2020 at 14:00 Helsinki Timezone) I will be giving a tutorial on MaxSAT at the ECAI 2020 conference together with Matti Järvisalo and Ruben Martins. The event is virtual and attendance is free, so any interested people should attend.

I am looking forward to the (new) experience of giving a tutorial, I am happy with the material and am sure we will be able to tech people about modern MaxSAT in an affective way.

New papers accepted

Leave a reply

The new decade has started well for me with two accepted publications already.
The first one, Preprocessing in Incomplete MaxSAT Solving is joint work with Marcus Leivo and Matti järvisalo, and is also Marcus first publication! The paper investigates the effect that preprocessing has on the non-optimal solutions of MAxSAT instances. The paper ties  my recent work on incomplete MaxSAT solving with my earlier work on MaxSAT preprocessing and I am very excited to push this line of research further. It will be published in the proceedings of the 2020 ECAI conference. I will most likely be travelling there myself to present this work, we are also looking into proposing a tutorial for the conference.

The second paper, Core-Guided and Core-Boosted Search for CP, extends and generalises my work on incomplete MaxSAT solving to the more general finite domain constraint programming paradigm. The paper is joint work with Graeme Grange, Emir Demirovic and Peter Stuckey from Australia. I am surprised and pleased to see that our previous work on MaxSAT seems to work so well in CP solving as well. The paper will be published in the proceedings of the 2020 CPAIOR conference. I will most likely not travel there myself, but I am sure that my co-authors will do the paper justice.

I’d like to thank all my co-authors for their work, it’s been a pleasure collaborating and hopefully we can continue doing so. The papers will be added to this webpage when the publishing process is done. If you want to read them earlier, feel free to send me an e-mail.

Excellent performance in the MaxSAT Evaluation

Leave a reply

The MaxSAT Evaluation is an annual event meant to evaluate the state of the art in MaxSAT solving technology. The evaluation has two tracks: the complete track, where the goal is to find the provably optimal solution as fast as possible and the incomplete track where the goal is to find a solution which is as good as possible within a limited time.

This year we submitted a solver called Loandra to the incomplete track of the competition. Loandra implements core boosted linear search, an idea described in this paper that I worked on during my visit to Melbourne last fall. The results of the Evaluations were presented yesterday at the SAT conference, I’ve only seen a summary but I am happy to say that Loandra performed very well, achieving the highest score on the unweighted 300s track and the second to highest on the weighted 300s track. Overall a very nice result, I am very pleased.

I’d like to thank the organizers of the MaxSAT evaluation as well as my co-authors, Emir Demirovic and Peter Stuckey! I am currently on a holiday, but once I get back I will put up Loandra on github as well. It will also eventually be made available here.

EDIT: Loandra is now available at: https://github.com/jezberg/loandra and on the software pages.

 

A new publication

Leave a reply

My paper “Unifying Reasoning and Core-Guided Search for Maximum Satisfiability” got accepted for publication at JELIA 2019. The paper reports on a theoretical investigation of the correctness MaxSAT solving techniques that can be seen as instance transformations. In fact, many approaches to MaxSAT solving transform a MaxSAT instance to be solved while preserving an optimal solution until the optimal solution is in some sense “trivial” to find (details in the paper).
We show that previously established theoretical notions for establishing the correctness of such methods are not general enough to capture all modern MaxSAT solving techniques, thus making the development of solvers that combine different methods difficult. We also propose a new type of instance transformation that covers all previously proposed notions that we are aware off. Finally we also generalize some known results from reasoning techniques from SAT solving to MaxSAT, thus bridging the gap between SAT solving and MaxSAT solving.
I am exited about this line of work, it feels like there is more to understand in this direction, hopefully I can extend this work in the near future.