13 Search Results for "Järvisalo, Matti"

Document
DOI: 10.4230/LIPIcs.CP.2023.18
Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization

Authors: Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and Matti Järvisalo

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract
Building on Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT) solving algorithms, several approaches to computing Pareto-optimal MaxSAT solutions under multiple objectives have been recently proposed. However, preprocessing in (Max)SAT-based multi-objective optimization remains so-far unexplored. Generalizing clause redundancy to the multi-objective setting, we establish provably-correct liftings of MaxSAT preprocessing techniques for multi-objective MaxSAT in terms of computing Pareto-optimal solutions. We also establish preservation of Pareto-MCSes - the multi-objective lifting of minimal correction sets tightly connected to optimal MaxSAT solutions - as a distinguishing feature between different redundancy notions in the multi-objective setting. Furthermore, we provide a first empirical evaluation of the effect of preprocessing on instance sizes and multi-objective MaxSAT solvers.
Cite as

Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and Matti Järvisalo. Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 18:1-18:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jabs_et_al:LIPIcs.CP.2023.18,
  author =	{Jabs, Christoph and Berg, Jeremias and Ihalainen, Hannes and J\"{a}rvisalo, Matti},
  title =	{{Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.18},
  URN =		{urn:nbn:de:0030-drops-190553},
  doi =		{10.4230/LIPIcs.CP.2023.18},
  annote =	{Keywords: maximum satisfiability, multi-objective combinatorial optimization, preprocessing, redundancy}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.1
Engineering a Preprocessor for Symmetry Detection

Authors: Markus Anders, Pascal Schweitzer, and Julian Stieß

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
State-of-the-art solvers for symmetry detection in combinatorial objects are becoming increasingly sophisticated software libraries. Most of the solvers were initially designed with inputs from combinatorics in mind (nauty, bliss, Traces, dejavu). They excel at dealing with a complicated core of the input. Others focus on practical instances that exhibit sparsity. They excel at dealing with comparatively easy but extremely large substructures of the input (saucy). In practice, these differences manifest in significantly diverging performances on different types of graph classes. We engineer a preprocessor for symmetry detection. The result is a tool designed to shrink sparse, large substructures of the input graph. On most of the practical instances, the preprocessor improves the overall running time significantly for many of the state-of-the-art solvers. At the same time, our benchmarks show that the additional overhead is negligible. Overall we obtain single algorithms with competitive performance across all benchmark graphs. As such, the preprocessor bridges the disparity between solvers that focus on combinatorial graphs and large practical graphs. In fact, on most of the practical instances the combined setup significantly outperforms previous state-of-the-art.
Cite as

Markus Anders, Pascal Schweitzer, and Julian Stieß. Engineering a Preprocessor for Symmetry Detection. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 1:1-1:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SEA.2023.1,
  author =	{Anders, Markus and Schweitzer, Pascal and Stie{\ss}, Julian},
  title =	{{Engineering a Preprocessor for Symmetry Detection}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.1},
  URN =		{urn:nbn:de:0030-drops-183511},
  doi =		{10.4230/LIPIcs.SEA.2023.1},
  annote =	{Keywords: graph isomorphism, automorphism groups, symmetry detection, preprocessors}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.15
FREIGHT: Fast Streaming Hypergraph Partitioning

Authors: Kamal Eyubov, Marcelo Fonseca Faraj, and Christian Schulz

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
Partitioning the vertices of a (hyper)graph into k roughly balanced blocks such that few (hyper)edges run between blocks is a key problem for large-scale distributed processing. A current trend for partitioning huge (hyper)graphs using low computational resources are streaming algorithms. In this work, we propose FREIGHT: a Fast stREamInG Hypergraph parTitioning algorithm which is an adaptation of the widely-known graph-based algorithm Fennel. By using an efficient data structure, we make the overall running of FREIGHT linearly dependent on the pin-count of the hypergraph and the memory consumption linearly dependent on the numbers of nets and blocks. The results of our extensive experimentation showcase the promising performance of FREIGHT as a highly efficient and effective solution for streaming hypergraph partitioning. Our algorithm demonstrates competitive running time with the Hashing algorithm, with a difference of a maximum factor of four observed on three fourths of the instances. Significantly, our findings highlight the superiority of FREIGHT over all existing (buffered) streaming algorithms and even the in-memory algorithm HYPE, with respect to both cut-net and connectivity measures. This indicates that our proposed algorithm is a promising hypergraph partitioning tool to tackle the challenge posed by large-scale and dynamic data processing.
Cite as

Kamal Eyubov, Marcelo Fonseca Faraj, and Christian Schulz. FREIGHT: Fast Streaming Hypergraph Partitioning. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 15:1-15:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{eyubov_et_al:LIPIcs.SEA.2023.15,
  author =	{Eyubov, Kamal and Fonseca Faraj, Marcelo and Schulz, Christian},
  title =	{{FREIGHT: Fast Streaming Hypergraph Partitioning}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.15},
  URN =		{urn:nbn:de:0030-drops-183657},
  doi =		{10.4230/LIPIcs.SEA.2023.15},
  annote =	{Keywords: Hypergraph partitioning, graph partitioning, edge partitioning, streaming}
}
Document
DOI: 10.4230/LIPIcs.SEA.2023.17
Greedy Heuristics for Judicious Hypergraph Partitioning

Authors: Noah Wahl and Lars Gottesbüren

Published in: LIPIcs, Volume 265, 21st International Symposium on Experimental Algorithms (SEA 2023)

Abstract
We investigate the efficacy of greedy heuristics for the judicious hypergraph partitioning problem. In contrast to balanced partitioning problems, the goal of judicious hypergraph partitioning is to minimize the maximum load over all blocks of the partition. We devise strategies for initial partitioning and FM-style post-processing. In combination with a multilevel scheme, they beat the previous state-of-the-art solver - based on greedy set covers - in both running time (two to four orders of magnitude) and solution quality (18% to 45%). A major challenge that makes local greedy approaches difficult to use for this problem is the high frequency of zero-gain moves, for which we present and evaluate counteracting mechanisms.
Cite as

Noah Wahl and Lars Gottesbüren. Greedy Heuristics for Judicious Hypergraph Partitioning. In 21st International Symposium on Experimental Algorithms (SEA 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 265, pp. 17:1-17:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{wahl_et_al:LIPIcs.SEA.2023.17,
  author =	{Wahl, Noah and Gottesb\"{u}ren, Lars},
  title =	{{Greedy Heuristics for Judicious Hypergraph Partitioning}},
  booktitle =	{21st International Symposium on Experimental Algorithms (SEA 2023)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-279-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{265},
  editor =	{Georgiadis, Loukas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2023.17},
  URN =		{urn:nbn:de:0030-drops-183674},
  doi =		{10.4230/LIPIcs.SEA.2023.17},
  annote =	{Keywords: hypergraph partitioning, local search algorithms, load balancing, local search}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.12
MaxSAT-Based Bi-Objective Boolean Optimization

Authors: Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
We explore a maximum satisfiability (MaxSAT) based approach to bi-objective optimization. Bi-objective optimization refers to the task of finding so-called Pareto-optimal solutions in terms of two objective functions. Bi-objective optimization problems naturally arise in various real-world settings. For example, in the context of learning interpretable representations, such as decision rules, from data, one wishes to balance between two objectives, the classification error and the size of the representation. Our approach is generally applicable to bi-objective optimizations which allow for propositional encodings. The approach makes heavy use of incremental Boolean satisfiability (SAT) solving and draws inspiration from modern MaxSAT solving approaches. In particular, we describe several variants of the approach which arise from different approaches to MaxSAT solving. In addition to computing a single representative solution per each point of the Pareto front, the approach allows for enumerating all Pareto-optimal solutions. We empirically compare the efficiency of the approach to recent competing approaches, showing practical benefits of our approach in the contexts of learning interpretable classification rules and bi-objective set covering.
Cite as

Christoph Jabs, Jeremias Berg, Andreas Niskanen, and Matti Järvisalo. MaxSAT-Based Bi-Objective Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 12:1-12:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jabs_et_al:LIPIcs.SAT.2022.12,
  author =	{Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J\"{a}rvisalo, Matti},
  title =	{{MaxSAT-Based Bi-Objective Boolean Optimization}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.12},
  URN =		{urn:nbn:de:0030-drops-166863},
  doi =		{10.4230/LIPIcs.SAT.2022.12},
  annote =	{Keywords: Multi-objective optimization, Pareto front enumeration, bi-objective optimization, maximum satisfiability, incremental SAT}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.13
Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization

Authors: Pavel Smirnov, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
The development of practical approaches to efficiently reasoning over pseudo-Boolean constraints has recently increasing attention as a natural generalization of Boolean satisfiability (SAT) solving. Analogously, solvers for pseudo-Boolean optimization draw inspiration from techniques developed for maximum satisfiability (MaxSAT) solving. Recently, the first practical solver lifting the implicit hitting set (IHS) approach - one of the most efficient approaches in modern MaxSAT solving - to the realm of PBO was developed, employing a PB solver as a core extractor together with an integer programming solver as a hitting set solver. In this work, we make practical improvements to the IHS approach to PBO. We propose the integration of solution-improving search to the PBO-IHS approach, resulting in a hybrid approach to PBO which makes use of both types of search towards an optimal solution. Furthermore, we explore the potential of different variants of core extraction within PBO-IHS - including recent advances in PB core extraction, allowing for extracting more general PB constraints compared to the at-least-one constraints typically relied on in IHS - in speeding up PBO-IHS search. We show that the empirical efficiency of PBO-IHS - recently shown to outperform other specialized PBO solvers - is further improved by the integration of these techniques.
Cite as

Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 13:1-13:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{smirnov_et_al:LIPIcs.SAT.2022.13,
  author =	{Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.13},
  URN =		{urn:nbn:de:0030-drops-166871},
  doi =		{10.4230/LIPIcs.SAT.2022.13},
  annote =	{Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets, solution-improving search, unsatisfiable cores}
}
Document
DOI: 10.4230/LIPIcs.SAT.2022.14
Incremental Maximum Satisfiability

Authors: Andreas Niskanen, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract
Boolean satisfiability (SAT) solvers allow for incremental computations, which is key to efficient employment of SAT solvers iteratively for developing complex decision and optimization procedures, including maximum satisfiability (MaxSAT) solvers. However, enabling incremental computations on the level of constraint optimization remains a noticeable challenge. While incremental computations have been identified to have great potential in speeding up MaxSAT-based approaches for solving various real-world optimization problems, enabling incremental computations in MaxSAT remains to most extent unexplored. In this work, we contribute towards making incremental MaxSAT solving a reality. Firstly, building on the IPASIR interface for incremental SAT solving, we propose the IPAMIR interface for implementing incremental MaxSAT solvers and for developing applications making use of incremental MaxSAT. Secondly, we expand our recent adaptation of the implicit hitting set based MaxHS MaxSAT solver to a fully-fledged incremental MaxSAT solver in terms of implementing the IPAMIR specification in full, and detail in particular how, in addition to weight changes, assumptions are enabled without losing incrementality. Thirdly, we provide further empirical evidence on the benefits of incremental MaxSAT solving under assumptions.
Cite as

Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Incremental Maximum Satisfiability. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 14:1-14:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{niskanen_et_al:LIPIcs.SAT.2022.14,
  author =	{Niskanen, Andreas and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Incremental Maximum Satisfiability}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.14},
  URN =		{urn:nbn:de:0030-drops-166885},
  doi =		{10.4230/LIPIcs.SAT.2022.14},
  annote =	{Keywords: maximum satisfiability, MaxSAT, incremental optimization, API, implicit hitting set approach}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2021.8
Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper)

Authors: Tuukka Korhonen and Matti Järvisalo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Propositional model counting (#SAT), the problem of determining the number of satisfying assignments of a propositional formula, is the archetypical #P-complete problem with a wide range of applications in AI. In this paper, we show that integrating tree decompositions of low width into the decision heuristics of a reference exact model counter (SharpSAT) significantly improves its runtime performance. In particular, our modifications to SharpSAT (and its derivant GANAK) lift the runtime efficiency of SharpSAT to the extent that it outperforms state-of-the-art exact model counters, including earlier-developed model counters that exploit tree decompositions.
Cite as

Tuukka Korhonen and Matti Järvisalo. Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 8:1-8:11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{korhonen_et_al:LIPIcs.CP.2021.8,
  author =	{Korhonen, Tuukka and J\"{a}rvisalo, Matti},
  title =	{{Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{8:1--8:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.8},
  URN =		{urn:nbn:de:0030-drops-152992},
  doi =		{10.4230/LIPIcs.CP.2021.8},
  annote =	{Keywords: propositional model counting, decision heuristics, tree decompositions, empirical evaluation}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.28
Refined Core Relaxation for Core-Guided MaxSAT Solving

Authors: Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Maximum satisfiability (MaxSAT) is a viable approach to solving NP-hard optimization problems. In the realm of core-guided MaxSAT solving - one of the most effective MaxSAT solving paradigms today - algorithmic variants employing so-called soft cardinality constraints have proven very effective. In this work, we propose to combine weight-aware core extraction (WCE) - a recently proposed approach that enables relaxing multiple cores instead of a single one during iterations of core-guided search - with a novel form of structure sharing in the cardinality-based core relaxation steps performed in core-guided MaxSAT solvers. In particular, the proposed form of structure sharing is enabled by WCE, which has so-far not been widely integrated to MaxSAT solvers, and allows for introducing fewer variables and clauses during the MaxSAT solving process. Our results show that 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. In particular, the combination of WCE and structure sharing improves the runtime performance of a state-of-the-art core-guided MaxSAT solver implementing the central OLL algorithm.
Cite as

Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Refined Core Relaxation for Core-Guided MaxSAT Solving. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 28:1-28:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.CP.2021.28,
  author =	{Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Refined Core Relaxation for Core-Guided MaxSAT Solving}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.28},
  URN =		{urn:nbn:de:0030-drops-153197},
  doi =		{10.4230/LIPIcs.CP.2021.28},
  annote =	{Keywords: maximum satisfiability, MaxSAT, core-guided MaxSAT solving}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.44
Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights

Authors: Andreas Niskanen, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Recent advances in solvers for the Boolean satisfiability (SAT) based optimization paradigm of maximum satisfiability (MaxSAT) have turned MaxSAT into a viable approach to finding provably optimal solutions for various types of hard optimization problems. In various types of real-world problem settings, a sequence of related optimization problems need to solved. This calls for studying ways of enabling incremental computations in MaxSAT, with the hope of speeding up the overall computation times. However, current state-of-the-art MaxSAT solvers offer no or limited forms of incrementality. In this work, we study ways of enabling incremental computations in the context of the implicit hitting set (IHS) approach to MaxSAT solving, as both one of the key MaxSAT solving approaches today and a relatively well-suited candidate for extending to incremental computations. In particular, motivated by several recent applications of MaxSAT in the context of interpretability in machine learning calling for this type of incrementality, we focus on enabling incrementality in IHS under changes to the objective function coefficients (i.e., to the weights of soft clauses). To this end, we explain to what extent different search techniques applied in IHS-based MaxSAT solving can and cannot be adapted to this incremental setting. As practical result, we develop an incremental version of an IHS MaxSAT solver, and show it provides significant runtime improvements in recent application settings which can benefit from incrementality but 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.
Cite as

Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 44:1-44:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{niskanen_et_al:LIPIcs.CP.2021.44,
  author =	{Niskanen, Andreas and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{44:1--44:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.44},
  URN =		{urn:nbn:de:0030-drops-153354},
  doi =		{10.4230/LIPIcs.CP.2021.44},
  annote =	{Keywords: Constraint optimization, maximum satisfiability, MaxSAT, implicit hitting set approach}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.51
Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors: Pavel Smirnov, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Recent developments in applying and extending Boolean satisfiability (SAT) based techniques have resulted in new types of approaches to pseudo-Boolean optimization (PBO), complementary to the more classical integer programming techniques. In this paper, we develop the first approach to pseudo-Boolean optimization based on instantiating the so-called implicit hitting set (IHS) approach, motivated by the success of IHS implementations for maximum satisfiability (MaxSAT). In particular, we harness recent advances in native reasoning techniques for pseudo-Boolean constraints, which enable efficiently identifying inconsistent assignments over subsets of objective function variables (i.e. unsatisfiable cores in the context of PBO), as a basis for developing a native IHS approach to PBO, and study the impact of various search techniques applicable in the context of IHS for PBO. Through an extensive empirical evaluation, we show that the IHS approach to PBO can outperform other currently available PBO solvers, and also provides a complementary approach to PBO when compared to classical integer programming techniques.
Cite as

Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Pseudo-Boolean Optimization by Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 51:1-51:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{smirnov_et_al:LIPIcs.CP.2021.51,
  author =	{Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{51:1--51:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.51},
  URN =		{urn:nbn:de:0030-drops-153429},
  doi =		{10.4230/LIPIcs.CP.2021.51},
  annote =	{Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2021.87
Lower Bounds on Dynamic Programming for Maximum Weight Independent Set

Authors: Tuukka Korhonen

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We prove lower bounds on pure dynamic programming algorithms for maximum weight independent set (MWIS). We model such algorithms as tropical circuits, i.e., circuits that compute with max and + operations. For a graph G, an MWIS-circuit of G is a tropical circuit whose inputs correspond to vertices of G and which computes the weight of a maximum weight independent set of G for any assignment of weights to the inputs. We show that if G has treewidth w and maximum degree d, then any MWIS-circuit of G has 2^{Ω(w/d)} gates and that if G is planar, or more generally H-minor-free for any fixed graph H, then any MWIS-circuit of G has 2^{Ω(w)} gates. An MWIS-formula is an MWIS-circuit where each gate has fan-out at most one. We show that if G has treedepth t and maximum degree d, then any MWIS-formula of G has 2^{Ω(t/d)} gates. It follows that treewidth characterizes optimal MWIS-circuits up to polynomials for all bounded degree graphs and H-minor-free graphs, and treedepth characterizes optimal MWIS-formulas up to polynomials for all bounded degree graphs.
Cite as

Tuukka Korhonen. Lower Bounds on Dynamic Programming for Maximum Weight Independent Set. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 87:1-87:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{korhonen:LIPIcs.ICALP.2021.87,
  author =	{Korhonen, Tuukka},
  title =	{{Lower Bounds on Dynamic Programming for Maximum Weight Independent Set}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{87:1--87:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.87},
  URN =		{urn:nbn:de:0030-drops-141562},
  doi =		{10.4230/LIPIcs.ICALP.2021.87},
  annote =	{Keywords: Maximum weight independent set, Treewidth, Tropical circuits, Dynamic programming, Treedepth, Monotone circuit complexity}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2020.22
Finding Optimal Triangulations Parameterized by Edge Clique Cover

Authors: Tuukka Korhonen

Published in: LIPIcs, Volume 180, 15th International Symposium on Parameterized and Exact Computation (IPEC 2020)

Abstract
Many graph problems can be formulated as a task of finding an optimal triangulation of a given graph with respect to some notion of optimality. In this paper we give algorithms to such problems parameterized by the size of a minimum edge clique cover (cc) of the graph. The parameter cc is both natural and well-motivated in many problems on this setting. For example, in the perfect phylogeny problem cc is at most the number of taxa, in fractional hypertreewidth cc is at most the number of hyperedges, and in treewidth of Bayesian networks cc is at most the number of non-root nodes of the Bayesian network. Our results are based on the framework of potential maximal cliques. We show that the number of minimal separators of graphs is at most 2^cc and the number of potential maximal cliques is at most 3^cc. Furthermore, these objects can be listed in times O^*(2^cc) and O^*(3^cc), respectively, even when no edge clique cover is given as input; the O^*(⋅) notation omits factors polynomial in the input size. Using these enumeration algorithms we obtain O^*(3^cc) time algorithms for problems in the potential maximal clique framework, including for example treewidth, minimum fill-in, and feedback vertex set. We also obtain an O^*(3^m) time algorithm for fractional hypertreewidth, where m is the number of hyperedges. In the case when an edge clique cover of size cc' is given as an input we further improve the time complexity to O^*(2^cc') for treewidth, minimum fill-in, and chordal sandwich. This implies an O^*(2^n) time algorithm for perfect phylogeny, where n is the number of taxa. We also give polynomial space algorithms with time complexities O^*(9^cc') and O^*(9^(cc + O(log^2 cc))) for problems in this framework.
Cite as

Tuukka Korhonen. Finding Optimal Triangulations Parameterized by Edge Clique Cover. In 15th International Symposium on Parameterized and Exact Computation (IPEC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 180, pp. 22:1-22:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{korhonen:LIPIcs.IPEC.2020.22,
  author =	{Korhonen, Tuukka},
  title =	{{Finding Optimal Triangulations Parameterized by Edge Clique Cover}},
  booktitle =	{15th International Symposium on Parameterized and Exact Computation (IPEC 2020)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-172-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{180},
  editor =	{Cao, Yixin and Pilipczuk, Marcin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2020.22},
  URN =		{urn:nbn:de:0030-drops-133253},
  doi =		{10.4230/LIPIcs.IPEC.2020.22},
  annote =	{Keywords: Treewidth, Minimum fill-in, Perfect phylogeny, Fractional hypertreewidth, Potential maximal cliques, Edge clique cover}
}
  • Refine by Author
  • 8 Järvisalo, Matti
  • 7 Berg, Jeremias
  • 3 Korhonen, Tuukka
  • 3 Niskanen, Andreas
  • 2 Ihalainen, Hannes
  • Show More...

  • Refine by Classification
  • 8 Theory of computation → Constraint and logic programming
  • 7 Mathematics of computing → Combinatorial optimization
  • 3 Theory of computation → Graph algorithms analysis
  • 2 Mathematics of computing → Graph algorithms
  • 1 Mathematics of computing → Hypergraphs
  • Show More...

  • Refine by Keyword
  • 5 maximum satisfiability
  • 3 MaxSAT
  • 2 Treewidth
  • 2 constraint optimization
  • 2 implicit hitting set approach
  • Show More...

  • Refine by Type
  • 13 document

  • Refine by Publication Year
  • 5 2021
  • 4 2023
  • 3 2022
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact