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.
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.
I am happy to let you know that I had three papers accepted at CP 2021. More details on them (as well as the full versions) can be found on on the publications page on these webpages.
I would like to thank all my co-authors, especially Pavel and Hannes whose first papers these are. See you at the conference in October!
These papers also mark the beginning of my very own Academy of Finland project! I am looking forward to developing new optimisation algorithms that combine the strengths and weaknesses of many different paradigms and also work incrementally.
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.
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.
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.
Our publication Solving Graph Problems via Potential Maximal Cliques: An Experimental Evaluation of the Bouchitté-Todinca Algorithm has been accepted for publication in the ACM Journal of Experimental Algorithmics. The article is currently in press, let me know if you are interested in reading it. I am the second author on this publication, with Tuukka Korhonen as the first and my PhD advisor Matti Järvisalo as the third.
The paper reports on an experimental evaluation of the so called Bouchitté-Todinca (BT) Algorithm for computing various graph parameters, including the treewidth and minimum fill of a graph. While the algorithm is the theoretically best known one for computing most of these parameters, there has not been many practical evaluations of it, most likely due to it being quite complicated to implement in practice. In this paper we provide an experimental evaluation of Tuukkas implementation that took second place in the minimum fill in track of the 2017 PACE challenge on 5 different graph problems. In the paper we show that Tuukas implementation of the BT algorithm is competitive with many previously proposed, problem specific algorithms, on all of the problems we consider. My role in this paper was to familiarize myself with and write about the theoretical foundations of the algorithm as well as provide input on what kind of experiments we should run. I liked working on this project as it allowed me to familiarize myself with something else than constraint programming.
Thanks to both Tuukka and Matti for their work in making this happen.