My Thesis won an Award

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.

MaxSAT tutorial at ECAI 2020

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.

Best Paper award at SAT 2020

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.

Supervising Master’s Theses

This spring was the first time I co-supervised Master’s theses. In total three students got their theses accepted during June:

I’d like to congratulate all students on finishing their theses. Even if I had supervised Bachelor’s theses before, supervising Master’s level students was a new experience for me. I learned a lot and can only hope I could provide useful supervision for them as well.

New paper accepted

I am happy to inform you that my paper “Abstract Cores in Implicit Hitting Set MaxSat Solving” has been accepted to the SAT 2020 conference.

The paper proposes an improvement to the so called Implicit Hitting Set-based approach to exact MaxSAT solving. The paper summarises the work we did with professor Fahiem Bacchus and MSc, Alex Poole during my visit to Toronto last year. I am exited by the paper. Thanks to both of my co-authors!

I will add the paper to these pages once the camera ready version has been submitted.

 

New papers accepted

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.

New presentation

I gave a talk at the Logic Seminar of the department of Mathematics and Statistics today. I talked about the algorithmic benefits of using propositional logic when solving optimisation and decision problems. As a concrete example, I used the Bounded Treewidth Bayesian Network Structure Learning Problem that we worked on a few years ago. Please find my slides: here.

Thank you to the logic group for having me, it was both interesting and fun.

Excellent performance in the MaxSAT Evaluation

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.

 

The conferment ceremony of the Faculty of Philosophy

About a month ago I participated in the conferment ceremony of the Faculty of Philosophy, a formal, and very traditional three day celebration during which I was granted the rights to wear the symbols of my academic degree, a doctoral hat and a doctoral sword.
The three days were filled with dinners and other festivities, culminating in a formal ball and a night procession through the center of Helsinki. I’d like to thank all of the organizers of the event!  I had a great time. The ceremony will probably be up there amongst the most unique experiences of my life, I mean when I am I ever going to be a part of a que consisting of 200+ masters and doctors dancing through the streets of Helsinki again.

All of the pictures here were taken by the talented people at Bonafide Creatives. Check them out at: https://www.bonafideweddings.fi/.

 

My thesis won an award

My PhD thesis: Solving Optimization Problems via Maximum Satisfiability : Encodings and Re-Encodings (available from e-thesis) was awarded one of four doctoral dissertation awards for 2018 of The University of Helsinki. I am grateful and honoured by this recognition. Thank you to everyone who played a role in my nomination and congratulations to my three other fellow recipients.

More information can be found in the University’s own news story.