The Constraint Reasoning and Optimization group contributes to CP 2021 with four papers:
- Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters by Tuukka Korhonen and Matti Järvisalo considers the archetypical #P-complete problem of propositional model counting, and shows that integrating tree decompositions of low width into the decision heuristics of state-of-the-art exact propositional model counters results in lifting the efficiency of the counters. This technique is central to the performance of the SharpSAT-TD model counter which ranked first in both the weighted and unweighted tracks of the 2021 Model Counting Competition.
- Pseudo-Boolean Optimization by Implicit Hitting Sets by Pavel Smirnov, Jeremias Berg, and Matti Järvisalo develops the first approach to pseudo-Boolean optimization based on instantiating the so-called implicit hitting set (IHS) approach. An implementation of the approaches is shown to outperform other currently available PBO solvers, and also to provide a complementary approach to PBO when compared to classical integer programming techniques.
- Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT under Changing Weights by Andreas Niskanen, Jeremias Berg, and Matti Järvisalo studies ways of enabling incremental computations in the context of the implicit hitting set approach to MaxSAT solving, motivated by recent applications of MaxSAT in the context of interpretability in machine learning calling for incremental MaxSAT solving. The work provides and incremental extension of the state-of-the-art MaxHS MaxSAT solving, and shown that incremental computations result in significant runtime improvements in recent application settings in which MaxSAT solvers have so-far been applied only non-incrementally, i.e., by calling a MaxSAT solver from scratch after each change to the problem instance at hand.
- Refined Core Relaxation for Core-Guided MaxSAT Solving by Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo describes ways of improving the the cardinality-based core relaxation steps in so-called core-guided MaxSAT solvers. In particular, the proposed techniques allow for avoiding potential overheads in the context of soft cardinality constraint based core-guided MaxSAT solving both in theory and in practice.