13 Search Results for "Niskanen, Andreas"

Document
PACE Solver Description
DOI: 10.4230/LIPIcs.IPEC.2025.37
PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving

Authors: André Schidler

Published in: LIPIcs, Volume 358, 20th International Symposium on Parameterized and Exact Computation (IPEC 2025)

Abstract
This paper describes our hybrid MaxSAT and mixed integer programming approach for finding minimum hitting sets as submitted to the 2025 PACE challenge. We also discuss hitting set specific challenges, lower bounds, preprocessing and design choices.
Cite as

André Schidler. PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving. In 20th International Symposium on Parameterized and Exact Computation (IPEC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 358, pp. 37:1-37:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schidler:LIPIcs.IPEC.2025.37,
  author =	{Schidler, Andr\'{e}},
  title =	{{PACE Solver Description: Minimum Hitting Set Computation via Core-Guided MaxSAT Solving}},
  booktitle =	{20th International Symposium on Parameterized and Exact Computation (IPEC 2025)},
  pages =	{37:1--37:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-407-9},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{358},
  editor =	{Agrawal, Akanksha and van Leeuwen, Erik Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2025.37},
  URN =		{urn:nbn:de:0030-drops-251692},
  doi =		{10.4230/LIPIcs.IPEC.2025.37},
  annote =	{Keywords: hitting set, maxsat, core-guided}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.17
Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks

Authors: Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains, including systems biology, computational logic, and artificial intelligence. A crucial property of BNs is the presence of trap spaces - subspaces of the state space that, once entered, cannot be exited. Minimal trap spaces, in particular, play a significant role in analyzing the long-term behavior of BNs, making their efficient enumeration and counting essential. The fixed points in BNs are a special case of minimal trap spaces. In this work, we formulate several meaningful counting problems related to minimal trap spaces and fixed points in BNs. These problems provide valuable insights both within BN theory (e.g., in probabilistic reasoning and dynamical analysis) and in broader application areas, including systems biology, abstract argumentation, and logic programming. To address these computational challenges, we propose novel methods based on approximate answer set counting, leveraging techniques from answer set programming. Our approach efficiently approximates the number of minimal trap spaces and the number of fixed points without requiring exhaustive enumeration, making it particularly well-suited for large-scale BNs. Our experimental evaluation on an extensive and diverse set of benchmark instances shows that our methods significantly improve the feasibility of counting minimal trap spaces and fixed points, paving the way for new applications in BN analysis and beyond.
Cite as

Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva, and Kuldeep S Meel. Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 17:1-17:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kabir_et_al:LIPIcs.CP.2025.17,
  author =	{Kabir, Mohimenul and Trinh, Van-Giang and Pastva, Samuel and Meel, Kuldeep S},
  title =	{{Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{17:1--17:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.17},
  URN =		{urn:nbn:de:0030-drops-238780},
  doi =		{10.4230/LIPIcs.CP.2025.17},
  annote =	{Keywords: Computational systems biology, Boolean network, Fixed point, Trap space, Answer set counting, Projected counting, Abstract argumentation, Logic programming}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.15
Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets

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

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
We propose symmetric core learning (SCL) as a novel approach to making the implicit hitting set approach (IHS) to constraint optimization more symmetry-aware. SCL has the potential of significantly reducing the number of iterations and, in particular, the number of calls to an NP decision solver for extracting individual unsatisfiable cores. As the technique is focused on generating symmetric cores to the hitting set component of IHS, SCL is generally applicable in IHS-style search for essentially any constraint optimization paradigm. In this work, we focus in particular on integrating SCL to IHS for pseudo-Boolean optimization (PBO), as earlier proposed static symmetry breaking through lex-leader constraints generated before search turns out to often degrade the performance of the IHS approach to PBO. In contrast, we show that SCL can improve the runtime performance of a state-of-the-art IHS approach to PBO and generally does not impose significant overhead in terms of runtime performance.
Cite as

Hannes Ihalainen, Jeremias Berg, Matti Järvisalo, and Bart Bogaerts. Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 15:1-15:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.CP.2025.15,
  author =	{Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti and Bogaerts, Bart},
  title =	{{Symmetric Core Learning for Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{15:1--15:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.15},
  URN =		{urn:nbn:de:0030-drops-238767},
  doi =		{10.4230/LIPIcs.CP.2025.15},
  annote =	{Keywords: Implicit hitting sets, symmetries, unsatisfiable cores, pseudo-Boolean optimization}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.28
SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability

Authors: Ole Lübke and Jeremias Berg

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Maximum Satisfiability (MaxSAT), the constraint paradigm of minimizing a linear expression over Boolean (0-1) variables subject to a set of propositional clauses, is today used for solving NP-hard combinatorial optimization problems in various domains. Especially anytime MaxSAT solvers that compute low-cost solutions within a limited available computational time have significantly improved in recent years. Such solvers can be divided into SAT-based methods that use sophisticated reasoning, and stochastic local search (SLS) methods that heuristically explore the search space. The two are complementary; roughly speaking, SLS struggles with finding feasible solutions, and SAT-based methods with minimizing cost. Consequently, most state-of-the-art anytime MaxSAT solvers run SLS before a SAT-based algorithm with minimal communication between the two. In this paper, we aim to harness the complementary strengths of SAT-based, and SLS approaches in the context of anytime MaxSAT. More precisely, we describe several ways to enhance the performance of the so-called core-boosted linear search algorithm for anytime MaxSAT with SLS techniques. Core-boosted linear search is a three-phase algorithm where each phase uses different types of reasoning. Beyond MaxSAT, core-boosted search has also been successful in the related paradigms of pseudo-boolean optimization and constraint programming. We describe how an SLS approach to MaxSAT can be tightly integrated with all three phases of the algorithm, resulting in non-trivial information exchange in both directions between the SLS algorithm and the reasoning methods. We evaluate our techniques on standard benchmarks from the latest MaxSAT Evaluation and demonstrate that our techniques can noticeably improve on implementations of core-boosted search and SLS.
Cite as

Ole Lübke and Jeremias Berg. SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lubke_et_al:LIPIcs.CP.2025.28,
  author =	{L\"{u}bke, Ole and Berg, Jeremias},
  title =	{{SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.28},
  URN =		{urn:nbn:de:0030-drops-238897},
  doi =		{10.4230/LIPIcs.CP.2025.28},
  annote =	{Keywords: Maximum Satisfiability, MaxSAT, SAT, SLS, Anytime Optimization}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.15
RustSAT: A Library for SAT Solving in Rust

Authors: Christoph Jabs

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the low level syntax of SAT and the expert knowledge required to achieve tight integration with SAT solvers should be further reduced. We present RustSAT, a library with the aim of making SAT solving technology readily available in the Rust programming language. RustSAT provides functionality for helping with generating (Max)SAT instances, writing them to, or reading them from files. Furthermore, RustSAT includes interfaces to various state-of-the-art SAT solvers available with a unified Rust API. Lastly, RustSAT implements several encodings for higher level constraints (at-most-one, cardinality, and pseudo-Boolean), which are also available via a C and Python API.
Cite as

Christoph Jabs. RustSAT: A Library for SAT Solving in Rust. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 15:1-15:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jabs:LIPIcs.SAT.2025.15,
  author =	{Jabs, Christoph},
  title =	{{RustSAT: A Library for SAT Solving in Rust}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{15:1--15:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.15},
  URN =		{urn:nbn:de:0030-drops-237498},
  doi =		{10.4230/LIPIcs.SAT.2025.15},
  annote =	{Keywords: Rust, library, SAT solvers, constraint encodings}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.3
Problem Partitioning via Proof Prefixes

Authors: Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Satisfiability solvers have been instrumental in tackling hard problems, including mathematical challenges that require years of computation. A key obstacle in efficiently solving such problems lies in effectively partitioning them into many, frequently millions of subproblems. Existing automated partitioning techniques, primarily based on lookahead methods, perform well on some instances but fail to generate effective partitions for many others. This paper introduces a powerful partitioning approach that leverages prefixes of proofs derived from conflict-driven clause-learning solvers. This method enables non-experts to harness the power of massively parallel SAT solving for their problems. We also propose a semantically-driven partitioning technique tailored for problems with large cardinality constraints, which frequently arise in optimization tasks. We evaluate our methods on diverse benchmarks, including combinatorial problems and formulas from SAT and MaxSAT competitions. Our results demonstrate that these techniques outperform existing partitioning strategies in many cases, offering improved scalability and efficiency.
Cite as

Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule. Problem Partitioning via Proof Prefixes. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{battleman_et_al:LIPIcs.SAT.2025.3,
  author =	{Battleman, Zachary and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Problem Partitioning via Proof Prefixes}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.3},
  URN =		{urn:nbn:de:0030-drops-237378},
  doi =		{10.4230/LIPIcs.SAT.2025.3},
  annote =	{Keywords: Satisfiability solving, parallel computing, problem partitioning}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.26
Analyzing Reformulation Performance in Core-Guided MaxSAT Solving

Authors: André Schidler and Stefan Szeider

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Core-guided algorithms like OLL are among the best methods for solving the Maximum Satisfiability problem (MaxSAT). Although some performance characteristics of OLL have been studied, a comprehensive experimental analysis of its reformulation behavior is still missing. In this paper, we present a large-scale study on how different reformulations of a MaxSAT instance produced by OLL affect solver performance. By representing these reformulations as a directed acyclic graph (DAG), we isolate the impact of structural features - such as the size and interconnectivity of unsatisfiable cores - on solver runtime. Our extensive experimental evaluation of over 600k solver runs reveals clear correlations between DAG properties and performance outcomes. These results suggest a new avenue for designing heuristics that steer the solver toward more tractable reformulations. All OLL DAGs and performance data from our experiments are publicly available to foster further research.
Cite as

André Schidler and Stefan Szeider. Analyzing Reformulation Performance in Core-Guided MaxSAT Solving. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{schidler_et_al:LIPIcs.SAT.2025.26,
  author =	{Schidler, Andr\'{e} and Szeider, Stefan},
  title =	{{Analyzing Reformulation Performance in Core-Guided MaxSAT Solving}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.26},
  URN =		{urn:nbn:de:0030-drops-237605},
  doi =		{10.4230/LIPIcs.SAT.2025.26},
  annote =	{Keywords: maximum satisfiability, OLL, core-guided}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.23
Symbolic Conflict Analysis in Pseudo-Boolean Optimization

Authors: Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
In the the last two decades, a lot of effort has been devoted to the development of satisfiability-checking tools for a variety of SAT-related problems. However, most of these tools lack optimization capabilities. That is, instead of finding any solution, one is sometimes interested in a solution that is best according to some criterion. Pseudo-Boolean solvers can be used to deal with optimization by successively solving a series of problems that contain an additional pseudo-Boolean constraint expressing that a better solution is required. A key point for the success of this simple approach is that lemmas that are learned for one problem can be reused for subsequent ones. In this paper we go one step further and show how, by using a simple symbolic conflict analysis procedure, not only can lemmas be reused between problems but also strengthened, thus further pruning the search space traversal. In addition, we show how this technique automatically allows one to infer upper bounds in maximization problems, thus giving an estimation of how far the solver is from finding an optimal solution. Experimental results with our PB solver reveal that (i) this technique is indeed effective in practice, providing important speedups in problems where several solutions are found and (ii) on problems with very few solutions, where the impact of our technique is limited, its overhead is negligible.
Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Symbolic Conflict Analysis in Pseudo-Boolean Optimization. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2025.23,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
  title =	{{Symbolic Conflict Analysis in Pseudo-Boolean Optimization}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.23},
  URN =		{urn:nbn:de:0030-drops-237579},
  doi =		{10.4230/LIPIcs.SAT.2025.23},
  annote =	{Keywords: SAT, Pseudo-Boolean Optimization, Conflict Analysis}
}
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.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
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
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 Type
  • 13 Document/PDF
  • 8 Document/HTML

  • Refine by Publication Year
  • 8 2025
  • 2 2022
  • 2 2021
  • 1 2020

  • Refine by Author
  • 5 Berg, Jeremias
  • 4 Järvisalo, Matti
  • 3 Niskanen, Andreas
  • 2 Jabs, Christoph
  • 2 Korhonen, Tuukka
  • Show More...

  • Refine by Series/Journal
  • 13 LIPIcs

  • Refine by Classification
  • 8 Theory of computation → Constraint and logic programming
  • 5 Mathematics of computing → Combinatorial optimization
  • 3 Theory of computation → Automated reasoning
  • 2 Theory of computation → Graph algorithms analysis
  • 1 Applied computing → Systems biology
  • Show More...

  • Refine by Keyword
  • 4 maximum satisfiability
  • 3 MaxSAT
  • 2 SAT
  • 2 Treewidth
  • 2 core-guided
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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