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.