Publications

Here is a list of my scientific publications. I am more than happy to discuss any of these, just send me an e-mail. The full references can be found either on my DBLP or Google Scholar page.

All publications are peer-reviewed.

Journal Publications

Conference Publications

Notice that these publications are also peer reviewed.

  • Computing Smallest MUSes of Quantified Boolean Formulas, Andreas Niskanen, Jere Mustonen, Jeremias Berg and Matti Järvisalo. In Proceedings of LPNMR 2022
    • Presents an Implicit Hitting Set based approach for computing small unsatisfiable subsets of quantified Boolean formulas.
  • Clause Redundancy and Preprocessing in Maximum Satisfiability. Hannes Ihalainen, Jeremias Berg, Matti Järvisalo. In Proceedings of IJCAR 2022
    • Extends recent theory on clause redundancy in SAT solving to MaxSAT and extends the MaxPRE preprocessor with stronger reasoning techniques.
  • Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization. Pavel Smirnov, Jeremias Berg, Matti Järvisalo. In Proceedings of SAT 2022
    • Describes improvements to the algorithm for pseudo Boolean optimization we proposed in at CP2021. The improvements concern more general core extraction and adding solution improving (SAT/UNSAT) search.
  • MaxSAT-Based Bi-Objective Boolean Optimization. Christoph Jabs, Jeremias Berg, Andreas Niskanen, Matti Järvisalo. In Proceedings of SAT 2022
    • Describes a MaxSAT-based algorithm for bi-objective optimization and evaluates it on learning interpretable classifiers and set covering.
  • Incremental Maximum Satisfiability. Andreas Niskanen, Jeremias Berg, Matti Järvisalo. In Proceedings of SAT 2022
    • Describes an API for incremental MaxSAT computations and (to the best of my understanding) the first MaxSAT solver to fully suport incremental optimization under assumptions and weight changes.
  • Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT under Changing Weights. Andreas Niskanen, Jeremias Berg, Matti Järvisalo.  In Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP) 2021.
    • Proposes an algorithm for effectively computing optimal MaxSAT solutions with changing weights, a problem that finds applications in explainable AI, especially learning interpretable classifiers.
  • Refined Core Relaxation for Core-Guided MaxSAT Solving. Hannes Ihalainen, Jeremias Berg, Matti Järvisalo.  In Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP) 2021.
    • Describes an improvement to the core-relaxation steps done by core-guided MaxSAT algorithms. Builds on the 2017 CP paper.
  • Pseudo-Boolean Optimization by Implicit Hitting Sets. Pavel Smirnov,  Jeremias Berg, Matti Järvisalo. In Proceedings of the 27th International Conference on Principles and Practice of Constraint Programming (CP) 2021.
    • Proposes an implicit hitting set based algorithm for pseudo Boolean optimisation and evaluates it.
  • Abstract Cores in Implicit Hitting Set MaxSat Solving. Jeremias Berg, Fahiem Bacchus, Alex Poole. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT) 2020.
    • The work improves on the so called implicit hitting set approach to MaxSAT solving by introducing techniques from core-guided solving.
  • Core-Guided and Core-Boosted Search for CP. Graeme Gange, Jeremias Berg, Emir Demirovic and Peter Stuckey. In Proceedings of the 17th International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR) 2020.
    • The work generalises core-guided transformations from MaxSAT to Constraint Programming.
  • Preprocessing in Incomplete MaxSAT Solving. Marcus Leivo, Jeremias Berg and Matti Järvisalo. In Proceedings of the 24th European Conference on Artificial Intelligence (ECAI) 2020.
    • The work investigates the effect of preprocessing in the context of incomplete MaxSAT solving.
  • Enumerating Potential Maximal Cliques via SAT and ASP. Tuukka Korhonen, Jeremias Berg and Matti Järvisalo. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI) 2019.
    • The work proposes the use of declarative solvers for enumerating potential maximal cliques in the context of exact algorithms for computing different graph parameters (including treewidth but also others).
  • Unifying Reasoning and Core-Guided Search for Maximum Satisfiability. Jeremias Berg and Matti Järvisalo. In Proceedings of the 16th Edition of the European Conference on Logics in Artificial Intelligence (JELIA) 2019.
    • A theoretical study of the formalisms underlying core-guided MaxSAT solvers and MaxSAT preprocessing. A generic proof of correctness for lifting most SAT-based preprocessing techniques to MaxSAT.
  • Core-Boosted Linear Search for Incomplete MaxSAT. Jeremias Berg Emir Demirović and Peter Stuckey. In Proceedings of the 16th International Conference on the Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR) 2019.
    • Proposes core boosted linear search as a new hybrid search strategy for incomplete MaxSAT solving.
  • Minimum-Width Confidence Bands via Constraint Optimization. Jeremias Berg, Emilia Oikarinen, Matti Järvisalo, and Kai Puolamäki. In Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP), 2017.
    • Proposes and evaluates two constraint models for computing multivariate confidence intervals
  • Weight-Aware Core Extraction in SAT-Based MaxSAT Solving. Jeremias Berg and Matti Järvisalo. In Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP), 2017.
    • Proposes some alterations to the manner in which many core guided MaxSAT solvers extract unsatisfiable cores.
  • MaxPre: An Extended MaxSAT Preprocessor. Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo. In Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2017.
    • A tool description of MaxPre, the MaxSAT preprocessor developed in the CoReO research group.
    • The principal developer of MaxPre is Tuukka Korhonen
  • Subsumed Label Elimination for Maximum Satisfiability. Jeremias Berg, Paul Saikko, and Matti Järvisalo. In Proceedings of the 22nd European Conference on Artificial Intelligence (ECAI), 2016.
    • Proposes and evaluates a new preprocessing technique for MaxSAT
  • Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving. Jeremias Berg and Matti Järvisalo. In Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP), 2016.
    • A theoretical analysis of how preprocessing affects the number of iterations of MaxSAT solvers.
  • LMHS: A SAT-IP Hybrid MaxSAT Solver. Paul Saikko, Jeremias Berg, and Matti Järvisalo. Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), 2016.
    • Tool description of LMHS, a MaxSAT solver based on the implicit hitting set paradigm developed in the CoReO research group.
    • The principal developer of LMHS is Paul Saikko
  • Re-using Auxiliary Variables for MaxSAT Preprocessing. Jeremias Berg, Paul Saikko, and Matti Järvisalo. Proceedings of the IEEE 27th International Conference on Tools with Artificial Intelligence (ICTAI), 2015.
    • Proposes a slight generalization of the idea presented in the IJCAI 2015 publication.
  • Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT. Jeremias Berg, Paul Saikko, and Matti Järvisalo. In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI), 2015.
    • Proposes tighter integration between MaxSAT preprocessing and MaxSAT solving.
  • SAT-Based Approaches to Treewidth Computation: An Evaluation. Jeremias Berg and Matti Järvisalo. In Proceedings of the 2014 IEEE 26th International Conference on Tools with Artificial Intelligence (ICTAI), 2014.
    • Proposes and evaluates SAT and MaxSAT models for computing the treewidth of a graph.
  • Optimal Neighborhood Preserving Visualization by Maximum Satisfiability. Kerstin Bunte, Matti Järvisalo, Jeremias Berg, Petri Myllymäki, Jaakko Peltonen, and Samuel Kaski. In Proceedings of the 28th AAAI Conference on Artificial Intelligence AAAI, 2014.
    • Proposes and evaluates MaxSAT based methods for visualising data on a grid.
  • Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability. Jeremias Berg, Matti Järvisalo, and Brandon Malone. In Proceedings of the 17th International Conference on Artificial Intelligence and Statistics (AISTATS), 2014.
    • Proposes and evaluates a MaxSAT model for learning Bayesian Networks with bounded treewidth.

Workshop publications

Note that these are also peer-reviewed.

  • Applications of MaxSAT in Data Analysis. Jeremias Berg, Antti Hyttinen, and Matti Järvisalo. In Proceedings of the 6th Pragmatics of SAT Workshop (PoS), 2015.
    • Descriptions of unusual applications of MaxSAT.
  • Optimal Correlation Clustering via MaxSAT. Jeremias Berg and Matti Järvisalo. In Proceedings of the 2013 IEEE 13th International Conference on Data Mining Workshops (ICDMW), 2013.
    • Preliminary work on my master’s thesis and AIJ publication
    • Also the first conference I ever attended.

Theses

  • Solving Optimization Problems via Maximum Satisfiability: Encodings and Re-Encodings. Jeremias Berg, PhD thesis, University of Helsinki
    • Accepted with distinction on 12.6.2018
    • Awarded with one of the best thesis of 2018 awards of the University of Helsinki.
    • Awarded the 2020 ACP Doctoral Research Award
    • The thesis summarises most of my PhD research with emphasis on the following six publications.
      • Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT 
      • Re-using Auxiliary Variables for MaxSAT Preprocessing
      • Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving 
      • Subsumed Label Elimination for Maximum Satisfiability
      • Cost-Optimal Constrained Correlation Clustering via Weighted Partial Maximum Satisfiability
      • Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability
  • Cost-Optimal Correlation Clustering via Partial Maximum Satisfiability. Jeremias Berg, Master’s thesis, University of Helsinki
    • Accepted with Eximia Cum Laude Approbatur; the second possible highest grade, on 3.6.2014.
    • A preliminary version of the AIJ publication
  • Kromaattinen korrelaatioklusterointi Max-Sat-ongelmana (Chromatic Correlation Clustering as MaxSAT, in Finnish). Jeremias Berg, Bachelor’s thesis, University of Helsinki