publications

2024

1. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

   Jeremias Berg, Bart Bogaerts, Jakob Nordström, and 3 more authors

   In 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain,, 2024

   Abs PDF Code

   Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex “without loss of generality” arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce acertifying version of the state-of-the-art solver pacose with veripb proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.

2. From Single-Objective to Bi-Objective Maximum Satisfiability Solving

   Christoph Jabs, Jeremias Berg, Andreas Niskanen, and 1 more author

   Journal of Artificial Intelligence Research, 2024

   Abs PDF Code

   The declarative approach is key to efficiently finding optimal solutions to various types of NP-hard real-world combinatorial optimization problems. Most work on practical declarative solvers—ranging from classical integer programming to finite-domain constraint optimization and maximum satisfiability (MaxSAT)—has focused on optimization under a single objective; fewer advances have been made towards efficient declarative techniques for multi-objective optimization problems. Motivated by significant recent advances in practical solvers for MaxSAT, in this work we develop BiOptSat, an exact declarative approach for finding Pareto-optimal solutions to bi-objective optimization problems, with propositional logic as the underlying constraint language. BiOptSat can be viewed as an instantiation of the lexicographic method. The approach makes use of a single Boolean satisfiability solver that is incrementally employed throughout the entire search procedure, allowing for finding a single Pareto-optimal solution, finding one representative solution for each non-dominated point, and enumerating all Pareto-optimal solutions. We detail several algorithmic instantiations of BiOptSat, each building on recent algorithms proposed for single-objective MaxSAT. We empirically evaluate the instantiations compared to recently-proposed alternative approaches to multi-objective MaxSAT solving on several real-world domains from the literature, showing the practical benefits of our approach.

3. Unifying SAT-Based Approaches to Maximum Satisfiability Solving

   Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo

   Journal of Artificial Intelligence Research, 2024

   Abs PDF Code

   Maximum satisfiability (MaxSAT), employing propositional logic as the declarative language of choice, has turned into a viable approach to solving NP-hard optimization problems arising from artificial intelligence and other real-world settings. A key contributing factor to the success of MaxSAT is the rise of increasingly effective exact solvers that are based on iterative calls to a Boolean satisfiability (SAT) solver. The three types of SAT-based MaxSAT solving approaches, each with its distinguishing features, implemented in current state-of-the-art MaxSAT solvers are the core-guided, the implicit hitting set (IHS), and the objective-bounding approaches. The objective-bounding approach is based on directly searching over the objective function range by iteratively querying a SAT solver if the MaxSAT instance at hand has a solution under different bounds on the objective. In contrast, both core-guided and IHS are so-called unsatisfiability-based approaches that employ a SAT solver as an unsatisfiable core extractor to determine sources of inconsistencies, but critically differ in how the found unsatisfiable cores are made use of towards finding a provably optimal solution. Furthermore, a variety of different algorithmic variants of the core-guided approach in particular have been proposed and implemented in solvers. It is well-acknowledged that each of the three approaches has its advantages and disadvantages, which is also witnessed by instance and problem-domain specific runtime performance differences (and at times similarities) of MaxSAT solvers implementing variants of the approaches. However, the questions of to what extent the approaches are fundamentally different and how the benefits of the individual methods could be combined in a single algorithmic approach are currently not fully understood. In this work, we approach these questions by developing UniMaxSAT, a general unifying algorithmic framework. Based on the recent notion of abstract cores, UniMaxSAT captures in general core-guided, IHS and objective-bounding computations. The framework offers a unified way of establishing quite generally the correctness of the current approaches. We illustrate this by formally showing that UniMaxSAT can simulate the computations of various algorithmic instantiations of the three types of MaxSAT solving approaches. Furthermore, UniMaxSAT can be instantiated in novel ways giving rise to new algorithmic variants of the approaches. We illustrate this aspect by developing a prototype implementation of an algorithmic variant for MaxSAT based on the framework.

4. Certified MaxSAT Preprocessing

   Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, and 4 more authors

   In Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, 2024

   Abs DOI PDF Code

   Building on the progress in Boolean satisfiability (SAT) solving over the last decades, maximum satisfiability (MaxSAT) has become a viable approach for solving NP-hard optimization problems. However, ensuring correctness of MaxSAT solvers has remained a considerable concern. For SAT, this is largely a solved problem thanks to the use of proof logging, meaning that solvers emit machine-verifiable proofs to certify correctness. However, for MaxSAT, proof logging solvers have started being developed only very recently. Moreover, these nascent efforts have only targeted the core solving process, ignoring the preprocessing phase where input problem instances can be substantially reformulated before being passed on to the solver proper. In this work, we demonstrate how pseudo-Boolean proof logging can be used to certify the correctness of a wide range of modern MaxSAT preprocessing techniques. By combining and extending the VeriPB and CakePB tools, we provide formally verified end-to-end proof checking that the input and preprocessed output MaxSAT problem instances have the same optimal value. An extensive evaluation on applied MaxSAT benchmarks shows that our approach is feasible in practice.

5. Core Boosting in SAT-Based Multi-objective Optimization

   Christoph Jabs, Jeremias Berg, and Matti Järvisalo

   In Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 21st International Conference, CPAIOR 2024, Uppsala, Sweden, May 28-31, 2024, Proceedings, Part II, 2024

   Abs DOI PDF Code

   Maximum satisfiability (MaxSAT) constitutes today a successful approach to solving various real-world optimization problems through propositional encodings. Building on this success, approaches have recently been proposed for finding Pareto-optimal solutions to multi-objective MaxSAT (MO-MaxSAT) instances, i.e., propositional encodings under multiple objective functions. In this work, we propose \emphcore boosting as a reformulation/preprocessing technique for improving the runtime performance of MO-MaxSAT solvers. Core boosting in the multi-objective setting allows for shrinking the ranges of the multiple objectives at hand, which can be particularly beneficial for MO-MaxSAT relying on search that requires enforcing increasingly tighter objective bounds through propositional encodings. We show that core boosting is effective in improving the runtime performance of SAT-based MO-MaxSAT solvers typically with little overhead.

2023

1. Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization

   Christoph Jabs, Jeremias Berg, Hannes Ihalainen, and 1 more author

   In 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada, 2023

   Abs DOI Bib PDF Code

   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.

   @inproceedings{DBLP:conf/cp/JabsBIJ23,
     author = {Jabs, Christoph and Berg, Jeremias and Ihalainen, Hannes and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/JabsBIJ23.bib},
     booktitle = {29th International Conference on Principles and Practice of Constraint Programming, {CP} 2023, August 27-31, 2023, Toronto, Canada},
     date-added = {2024-01-18 20:06:33 +0200},
     date-modified = {2024-01-18 20:06:33 +0200},
     doi = {10.4230/LIPICS.CP.2023.18},
     editor = {Yap, Roland H. C.},
     pages = {18:1--18:20},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Sun, 12 Nov 2023 02:13:20 +0100},
     title = {Preprocessing in SAT-Based Multi-Objective Combinatorial Optimization},
     url = {https://doi.org/10.4230/LIPIcs.CP.2023.18},
     volume = {280},
     year = {2023},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.CP.2023.18}
   }

2. Certified Core-Guided MaxSAT Solving

   Jeremias Berg, Bart Bogaerts, Jakob Nordström, and 2 more authors

   In Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, 2023

   DOI Bib PDF

   @inproceedings{DBLP:conf/cade/BergBNOV23,
     author = {Berg, Jeremias and Bogaerts, Bart and Nordstr{\"{o}}m, Jakob and Oertel, Andy and Vandesande, Dieter},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cade/BergBNOV23.bib},
     booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings},
     date-added = {2024-01-18 20:06:24 +0200},
     date-modified = {2024-01-18 20:06:24 +0200},
     doi = {10.1007/978-3-031-38499-8\_1},
     editor = {Pientka, Brigitte and Tinelli, Cesare},
     pages = {1--22},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Thu, 14 Sep 2023 20:25:49 +0200},
     title = {Certified Core-Guided MaxSAT Solving},
     url = {https://doi.org/10.1007/978-3-031-38499-8\_1},
     volume = {14132},
     year = {2023},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-031-38499-8%5C_1}
   }

3. Oracle-Based Local Search for Pseudo-Boolean Optimization

   Markus Iser, Jeremias Berg, and Matti Järvisalo

   In ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland - Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS 2023), 2023

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/ecai/IserBJ23,
     author = {Iser, Markus and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ecai/IserBJ23.bib},
     booktitle = {{ECAI} 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Krak{\'{o}}w, Poland - Including 12th Conference on Prestigious Applications of Intelligent Systems {(PAIS} 2023)},
     doi = {10.3233/FAIA230387},
     editor = {Gal, Kobi and Now{\'{e}}, Ann and Nalepa, Grzegorz J. and Fairstein, Roy and Radulescu, Roxana},
     pages = {1124--1131},
     publisher = {{IOS} Press},
     series = {Frontiers in Artificial Intelligence and Applications},
     timestamp = {Thu, 09 Nov 2023 21:13:02 +0100},
     title = {Oracle-Based Local Search for Pseudo-Boolean Optimization},
     url = {https://doi.org/10.3233/FAIA230387},
     volume = {372},
     year = {2023},
     bdsk-url-1 = {https://doi.org/10.3233/FAIA230387}
   }

4. Unifying Core-Guided and Implicit Hitting Set Based Optimization

   Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo

   In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, 2023

   DOI Bib PDF

   @inproceedings{DBLP:conf/ijcai/IhalainenBJ23,
     author = {Ihalainen, Hannes and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ijcai/IhalainenBJ23.bib},
     booktitle = {Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, {IJCAI} 2023, 19th-25th August 2023, Macao, SAR, China},
     doi = {10.24963/IJCAI.2023/215},
     pages = {1935--1943},
     publisher = {ijcai.org},
     timestamp = {Mon, 28 Aug 2023 17:23:07 +0200},
     title = {Unifying Core-Guided and Implicit Hitting Set Based Optimization},
     url = {https://doi.org/10.24963/ijcai.2023/215},
     year = {2023},
     bdsk-url-1 = {https://doi.org/10.24963/ijcai.2023/215}
   }

2022

1. Clause Redundancy and Preprocessing in Maximum Satisfiability

   Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo

   In Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, 2022

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/cade/IhalainenBJ22,
     author = {Ihalainen, Hannes and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cade/IhalainenBJ22.bib},
     booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings},
     doi = {10.1007/978-3-031-10769-6\_6},
     editor = {Blanchette, Jasmin and Kov{\'{a}}cs, Laura and Pattinson, Dirk},
     pages = {75--94},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
     title = {Clause Redundancy and Preprocessing in Maximum Satisfiability},
     url = {https://doi.org/10.1007/978-3-031-10769-6\_6},
     volume = {13385},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-031-10769-6%5C_6}
   }

2. Computing Smallest MUSes of Quantified Boolean Formulas

   Andreas Niskanen, Jere Mustonen, Jeremias Berg, and 1 more author

   In Logic Programming and Nonmonotonic Reasoning - 16th International Conference, LPNMR 2022, Genova, Italy, September 5-9, 2022, Proceedings, 2022

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/lpnmr/NiskanenMBJ22,
     author = {Niskanen, Andreas and Mustonen, Jere and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/lpnmr/NiskanenMBJ22.bib},
     booktitle = {Logic Programming and Nonmonotonic Reasoning - 16th International Conference, {LPNMR} 2022, Genova, Italy, September 5-9, 2022, Proceedings},
     doi = {10.1007/978-3-031-15707-3\_23},
     editor = {Gottlob, Georg and Inclezan, Daniela and Maratea, Marco},
     pages = {301--314},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Wed, 07 Dec 2022 23:14:22 +0100},
     title = {Computing Smallest MUSes of Quantified Boolean Formulas},
     url = {https://doi.org/10.1007/978-3-031-15707-3\_23},
     volume = {13416},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-031-15707-3%5C_23}
   }

3. MaxSAT-Based Bi-Objective Boolean Optimization

   Christoph Jabs, Jeremias Berg, Andreas Niskanen, and 1 more author

   In 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, 2022

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/sat/JabsBNJ22,
     author = {Jabs, Christoph and Berg, Jeremias and Niskanen, Andreas and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/JabsBNJ22.bib},
     booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2022, August 2-5, 2022, Haifa, Israel},
     doi = {10.4230/LIPICS.SAT.2022.12},
     editor = {Meel, Kuldeep S. and Strichman, Ofer},
     pages = {12:1--12:23},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Sat, 30 Sep 2023 09:55:45 +0200},
     title = {MaxSAT-Based Bi-Objective Boolean Optimization},
     url = {https://doi.org/10.4230/LIPIcs.SAT.2022.12},
     volume = {236},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.SAT.2022.12}
   }

4. Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization

   Pavel Smirnov, Jeremias Berg, and Matti Järvisalo

   In 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, 2022

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/sat/0003BJ22,
     author = {Smirnov, Pavel and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/0003BJ22.bib},
     booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2022, August 2-5, 2022, Haifa, Israel},
     doi = {10.4230/LIPICS.SAT.2022.13},
     editor = {Meel, Kuldeep S. and Strichman, Ofer},
     pages = {13:1--13:18},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Thu, 28 Jul 2022 17:31:18 +0200},
     title = {Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization},
     url = {https://doi.org/10.4230/LIPIcs.SAT.2022.13},
     volume = {236},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.SAT.2022.13}
   }

5. Incremental Maximum Satisfiability

   Andreas Niskanen, Jeremias Berg, and Matti Järvisalo

   In 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, 2022

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/sat/NiskanenBJ22,
     author = {Niskanen, Andreas and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/NiskanenBJ22.bib},
     booktitle = {25th International Conference on Theory and Applications of Satisfiability Testing, {SAT} 2022, August 2-5, 2022, Haifa, Israel},
     doi = {10.4230/LIPICS.SAT.2022.14},
     editor = {Meel, Kuldeep S. and Strichman, Ofer},
     pages = {14:1--14:19},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Sun, 02 Oct 2022 16:14:34 +0200},
     title = {Incremental Maximum Satisfiability},
     url = {https://doi.org/10.4230/LIPIcs.SAT.2022.14},
     volume = {236},
     year = {2022},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.SAT.2022.14}
   }

2021

1. Refined Core Relaxation for Core-Guided MaxSAT Solving

   Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo

   In 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, 2021

   DOI Bib PDF Supp Code

   @inproceedings{DBLP:conf/cp/IhalainenBJ21,
     author = {Ihalainen, Hannes and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/IhalainenBJ21.bib},
     booktitle = {27th International Conference on Principles and Practice of Constraint Programming, {CP} 2021, Montpellier, France (Virtual Conference), October 25-29, 2021},
     doi = {10.4230/LIPICS.CP.2021.28},
     editor = {Michel, Laurent D.},
     pages = {28:1--28:19},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Wed, 03 Nov 2021 08:28:40 +0100},
     title = {Refined Core Relaxation for Core-Guided MaxSAT Solving},
     url = {https://doi.org/10.4230/LIPIcs.CP.2021.28},
     volume = {210},
     year = {2021},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.CP.2021.28}
   }

2. Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights

   Andreas Niskanen, Jeremias Berg, and Matti Järvisalo

   In 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, 2021

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/cp/NiskanenBJ21,
     author = {Niskanen, Andreas and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/NiskanenBJ21.bib},
     booktitle = {27th International Conference on Principles and Practice of Constraint Programming, {CP} 2021, Montpellier, France (Virtual Conference), October 25-29, 2021},
     doi = {10.4230/LIPICS.CP.2021.44},
     editor = {Michel, Laurent D.},
     pages = {44:1--44:19},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Wed, 03 Nov 2021 08:28:40 +0100},
     title = {Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights},
     url = {https://doi.org/10.4230/LIPIcs.CP.2021.44},
     volume = {210},
     year = {2021},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.CP.2021.44}
   }

3. Pseudo-Boolean Optimization by Implicit Hitting Sets

   Pavel Smirnov, Jeremias Berg, and Matti Järvisalo

   In 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, 2021

   DOI Bib PDF Supp Code

   @inproceedings{DBLP:conf/cp/SmirnovBJ21,
     author = {Smirnov, Pavel and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/SmirnovBJ21.bib},
     booktitle = {27th International Conference on Principles and Practice of Constraint Programming, {CP} 2021, Montpellier, France (Virtual Conference), October 25-29, 2021},
     doi = {10.4230/LIPICS.CP.2021.51},
     editor = {Michel, Laurent D.},
     pages = {51:1--51:20},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
     series = {LIPIcs},
     timestamp = {Thu, 04 Nov 2021 13:41:52 +0100},
     title = {Pseudo-Boolean Optimization by Implicit Hitting Sets},
     url = {https://doi.org/10.4230/LIPIcs.CP.2021.51},
     volume = {210},
     year = {2021},
     bdsk-url-1 = {https://doi.org/10.4230/LIPIcs.CP.2021.51}
   }

4. Abstract Cores in Implicit Hitting Set MaxSat Solving (Extended Abstract)

   Jeremias Berg, Fahiem Bacchus, and Alex Poole

   In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, 2021

   DOI Bib PDF Supp Code

   @inproceedings{DBLP:conf/ijcai/BergBP21,
     author = {Berg, Jeremias and Bacchus, Fahiem and Poole, Alex},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ijcai/BergBP21.bib},
     booktitle = {Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, {IJCAI} 2021, Virtual Event / Montreal, Canada, 19-27 August 2021},
     doi = {10.24963/IJCAI.2021/643},
     editor = {Zhou, Zhi{-}Hua},
     pages = {4745--4749},
     publisher = {ijcai.org},
     timestamp = {Wed, 25 Aug 2021 17:11:16 +0200},
     title = {Abstract Cores in Implicit Hitting Set MaxSat Solving (Extended Abstract)},
     url = {https://doi.org/10.24963/ijcai.2021/643},
     year = {2021},
     bdsk-url-1 = {https://doi.org/10.24963/ijcai.2021/643}
   }

2020

1. Core-Guided and Core-Boosted Search for CP

   Graeme Gange, Jeremias Berg, Emir Demirovic, and 1 more author

   In Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings, 2020

   DOI Bib PDF

   @inproceedings{DBLP:conf/cpaior/GangeBDS20,
     author = {Gange, Graeme and Berg, Jeremias and Demirovic, Emir and Stuckey, Peter J.},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cpaior/GangeBDS20.bib},
     booktitle = {Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 17th International Conference, {CPAIOR} 2020, Vienna, Austria, September 21-24, 2020, Proceedings},
     doi = {10.1007/978-3-030-58942-4\_14},
     editor = {Hebrard, Emmanuel and Musliu, Nysret},
     pages = {205--221},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Sun, 25 Oct 2020 23:15:05 +0100},
     title = {Core-Guided and Core-Boosted Search for {CP}},
     url = {https://doi.org/10.1007/978-3-030-58942-4\_14},
     volume = {12296},
     year = {2020},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-030-58942-4%5C_14}
   }

2. Preprocessing in Incomplete MaxSAT Solving

   Marcus Leivo, Jeremias Berg, and Matti Järvisalo

   In ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), 2020

   DOI Bib PDF Supp

   @inproceedings{DBLP:conf/ecai/LeivoBJ20,
     author = {Leivo, Marcus and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ecai/LeivoBJ20.bib},
     booktitle = {{ECAI} 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence {(PAIS} 2020)},
     doi = {10.3233/FAIA200112},
     editor = {Giacomo, Giuseppe De and Catal{\'{a}}, Alejandro and Dilkina, Bistra and Milano, Michela and Barro, Sen{\'{e}}n and Bugar{\'{\i}}n, Alberto and Lang, J{\'{e}}r{\^{o}}me},
     pages = {347--354},
     publisher = {{IOS} Press},
     series = {Frontiers in Artificial Intelligence and Applications},
     timestamp = {Fri, 09 Apr 2021 18:50:05 +0200},
     title = {Preprocessing in Incomplete MaxSAT Solving},
     url = {https://doi.org/10.3233/FAIA200112},
     volume = {325},
     year = {2020},
     bdsk-url-1 = {https://doi.org/10.3233/FAIA200112}
   }

3. Abstract Cores in Implicit Hitting Set MaxSat Solving

   Jeremias Berg, Fahiem Bacchus, and Alex Poole

   In Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, 2020

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/sat/BergBP20,
     author = {Berg, Jeremias and Bacchus, Fahiem and Poole, Alex},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/BergBP20.bib},
     booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings},
     doi = {10.1007/978-3-030-51825-7\_20},
     editor = {Pulina, Luca and Seidl, Martina},
     pages = {277--294},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Thu, 06 Aug 2020 21:49:45 +0200},
     title = {Abstract Cores in Implicit Hitting Set MaxSat Solving},
     url = {https://doi.org/10.1007/978-3-030-51825-7\_20},
     volume = {12178},
     year = {2020},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-030-51825-7%5C_20}
   }

2019

1. Solving Graph Problems via Potential Maximal Cliques: An Experimental Evaluation of the Bouchitté-Todinca Algorithm

   Tuukka Korhonen, Jeremias Berg, and Matti Järvisalo

   ACM J. Exp. Algorithmics, 2019

   DOI Bib

   @article{DBLP:journals/jea/KorhonenBJ19,
     author = {Korhonen, Tuukka and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/jea/KorhonenBJ19.bib},
     doi = {10.1145/3301297},
     journal = {{ACM} J. Exp. Algorithmics},
     number = {1},
     pages = {1.9:1--1.9:19},
     timestamp = {Thu, 14 Oct 2021 09:12:26 +0200},
     title = {Solving Graph Problems via Potential Maximal Cliques: An Experimental Evaluation of the Bouchitt{\'{e}}-Todinca Algorithm},
     url = {https://doi.org/10.1145/3301297},
     volume = {24},
     year = {2019},
     bdsk-url-1 = {https://doi.org/10.1145/3301297}
   }

2. Core-Boosted Linear Search for Incomplete MaxSAT

   Jeremias Berg, Emir Demirovic, and Peter J. Stuckey

   In Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4-7, 2019, Proceedings, 2019

   DOI Bib PDF Code

   @inproceedings{DBLP:conf/cpaior/BergDS19,
     author = {Berg, Jeremias and Demirovic, Emir and Stuckey, Peter J.},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cpaior/BergDS19.bib},
     booktitle = {Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 16th International Conference, {CPAIOR} 2019, Thessaloniki, Greece, June 4-7, 2019, Proceedings},
     doi = {10.1007/978-3-030-19212-9\_3},
     editor = {Rousseau, Louis{-}Martin and Stergiou, Kostas},
     pages = {39--56},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Tue, 28 May 2019 13:14:06 +0200},
     title = {Core-Boosted Linear Search for Incomplete MaxSAT},
     url = {https://doi.org/10.1007/978-3-030-19212-9\_3},
     volume = {11494},
     year = {2019},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-030-19212-9%5C_3}
   }

3. Enumerating Potential Maximal Cliques via SAT and ASP

   Tuukka Korhonen, Jeremias Berg, and Matti Järvisalo

   In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, 2019

   DOI Bib

   @inproceedings{DBLP:conf/ijcai/KorhonenBJ19,
     author = {Korhonen, Tuukka and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ijcai/KorhonenBJ19.bib},
     booktitle = {Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, {IJCAI} 2019, Macao, China, August 10-16, 2019},
     doi = {10.24963/IJCAI.2019/156},
     editor = {Kraus, Sarit},
     pages = {1116--1122},
     publisher = {ijcai.org},
     timestamp = {Thu, 14 Oct 2021 10:39:48 +0200},
     title = {Enumerating Potential Maximal Cliques via {SAT} and {ASP}},
     url = {https://doi.org/10.24963/ijcai.2019/156},
     year = {2019},
     bdsk-url-1 = {https://doi.org/10.24963/ijcai.2019/156}
   }

4. Unifying Reasoning and Core-Guided Search for Maximum Satisfiability

   Jeremias Berg, and Matti Järvisalo

   In Logics in Artificial Intelligence - 16th European Conference, JELIA 2019, Rende, Italy, May 7-11, 2019, Proceedings, 2019

   DOI Bib

   @inproceedings{DBLP:conf/jelia/BergJ19,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/jelia/BergJ19.bib},
     booktitle = {Logics in Artificial Intelligence - 16th European Conference, {JELIA} 2019, Rende, Italy, May 7-11, 2019, Proceedings},
     doi = {10.1007/978-3-030-19570-0\_19},
     editor = {Calimeri, Francesco and Leone, Nicola and Manna, Marco},
     pages = {287--303},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Fri, 27 Mar 2020 08:53:33 +0100},
     title = {Unifying Reasoning and Core-Guided Search for Maximum Satisfiability},
     url = {https://doi.org/10.1007/978-3-030-19570-0\_19},
     volume = {11468},
     year = {2019},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-030-19570-0%5C_19}
   }

2018

1. Solving Optimization Problems via Maximum Satisfiability: Encodings and Re-Encodings

   Jeremias Berg

   University of Helsinki, Finland, 2018

   Bib

   @phdthesis{DBLP:phd/basesearch/Berg18,
     author = {Berg, Jeremias},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/phd/basesearch/Berg18.bib},
     school = {University of Helsinki, Finland},
     timestamp = {Wed, 07 Dec 2022 23:29:31 +0100},
     title = {Solving Optimization Problems via Maximum Satisfiability: Encodings and Re-Encodings},
     url = {http://hdl.handle.net/10138/234642},
     year = {2018},
     bdsk-url-1 = {http://hdl.handle.net/10138/234642}
   }

2. Applications of MaxSAT in Data Analysis

   Jeremias Berg, Antti Hyttinen, and Matti Järvisalo

   In Proceedings of Pragmatics of SAT 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of SAT 2018, Oxford, UK, July 7, 2018, 2018

   DOI Bib

   @inproceedings{DBLP:conf/sat/BergHJ18,
     author = {Berg, Jeremias and Hyttinen, Antti and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/BergHJ18.bib},
     booktitle = {Proceedings of Pragmatics of {SAT} 2015, Austin, Texas, USA, September 23, 2015 / Pragmatics of {SAT} 2018, Oxford, UK, July 7, 2018},
     doi = {10.29007/3QKH},
     editor = {Berre, Daniel Le and J{\"{a}}rvisalo, Matti},
     pages = {50--64},
     publisher = {EasyChair},
     series = {EPiC Series in Computing},
     timestamp = {Sun, 15 Aug 2021 00:16:54 +0200},
     title = {Applications of MaxSAT in Data Analysis},
     url = {https://doi.org/10.29007/3qkh},
     volume = {59},
     year = {2018},
     bdsk-url-1 = {https://doi.org/10.29007/3qkh}
   }

2017

1. Cost-optimal constrained correlation clustering via weighted partial Maximum Satisfiability

   Jeremias Berg, and Matti Järvisalo

   Artif. Intell., 2017

   DOI Bib

   @article{DBLP:journals/ai/BergJ17,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/ai/BergJ17.bib},
     doi = {10.1016/J.ARTINT.2015.07.001},
     journal = {Artif. Intell.},
     pages = {110--142},
     timestamp = {Fri, 30 Nov 2018 13:29:20 +0100},
     title = {Cost-optimal constrained correlation clustering via weighted partial Maximum Satisfiability},
     url = {https://doi.org/10.1016/j.artint.2015.07.001},
     volume = {244},
     year = {2017},
     bdsk-url-1 = {https://doi.org/10.1016/j.artint.2015.07.001}
   }

2. Minimum-Width Confidence Bands via Constraint Optimization

   Jeremias Berg, Emilia Oikarinen, Matti Järvisalo, and 1 more author

   In Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, 2017

   DOI Bib

   @inproceedings{DBLP:conf/cp/BergOJP17,
     author = {Berg, Jeremias and Oikarinen, Emilia and J{\"{a}}rvisalo, Matti and Puolam{\"{a}}ki, Kai},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/BergOJP17.bib},
     booktitle = {Principles and Practice of Constraint Programming - 23rd International Conference, {CP} 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings},
     doi = {10.1007/978-3-319-66158-2\_29},
     editor = {Beck, J. Christopher},
     pages = {443--459},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Sat, 19 Oct 2019 20:32:31 +0200},
     title = {Minimum-Width Confidence Bands via Constraint Optimization},
     url = {https://doi.org/10.1007/978-3-319-66158-2\_29},
     volume = {10416},
     year = {2017},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-319-66158-2%5C_29}
   }

3. Weight-Aware Core Extraction in SAT-Based MaxSAT Solving

   Jeremias Berg, and Matti Järvisalo

   In Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, 2017

   DOI Bib

   @inproceedings{DBLP:conf/cp/BergJ17,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/BergJ17.bib},
     booktitle = {Principles and Practice of Constraint Programming - 23rd International Conference, {CP} 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings},
     doi = {10.1007/978-3-319-66158-2\_42},
     editor = {Beck, J. Christopher},
     pages = {652--670},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Tue, 14 May 2019 10:00:45 +0200},
     title = {Weight-Aware Core Extraction in SAT-Based MaxSAT Solving},
     url = {https://doi.org/10.1007/978-3-319-66158-2\_42},
     volume = {10416},
     year = {2017},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-319-66158-2%5C_42}
   }

4. MaxPre: An Extended MaxSAT Preprocessor

   Tuukka Korhonen, Jeremias Berg, Paul Saikko, and 1 more author

   In Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, 2017

   DOI Bib

   @inproceedings{DBLP:conf/sat/KorhonenBSJ17,
     author = {Korhonen, Tuukka and Berg, Jeremias and Saikko, Paul and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/KorhonenBSJ17.bib},
     booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings},
     doi = {10.1007/978-3-319-66263-3\_28},
     editor = {Gaspers, Serge and Walsh, Toby},
     pages = {449--456},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Thu, 14 Oct 2021 10:31:52 +0200},
     title = {MaxPre: An Extended MaxSAT Preprocessor},
     url = {https://doi.org/10.1007/978-3-319-66263-3\_28},
     volume = {10491},
     year = {2017},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-319-66263-3%5C_28}
   }

2016

1. Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving

   Jeremias Berg, and Matti Järvisalo

   In Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, 2016

   DOI Bib

   @inproceedings{DBLP:conf/cp/BergJ16,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/cp/BergJ16.bib},
     booktitle = {Principles and Practice of Constraint Programming - 22nd International Conference, {CP} 2016, Toulouse, France, September 5-9, 2016, Proceedings},
     doi = {10.1007/978-3-319-44953-1\_5},
     editor = {Rueher, Michel},
     pages = {66--85},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Tue, 14 May 2019 10:00:45 +0200},
     title = {Impact of SAT-Based Preprocessing on Core-Guided MaxSAT Solving},
     url = {https://doi.org/10.1007/978-3-319-44953-1\_5},
     volume = {9892},
     year = {2016},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-319-44953-1%5C_5}
   }

2. Subsumed Label Elimination for Maximum Satisfiability

   Jeremias Berg, Paul Saikko, and Matti Järvisalo

   In ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), 2016

   DOI Bib

   @inproceedings{DBLP:conf/ecai/BergSJ16,
     author = {Berg, Jeremias and Saikko, Paul and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ecai/BergSJ16.bib},
     booktitle = {{ECAI} 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence {(PAIS} 2016)},
     doi = {10.3233/978-1-61499-672-9-630},
     editor = {Kaminka, Gal A. and Fox, Maria and Bouquet, Paolo and H{\"{u}}llermeier, Eyke and Dignum, Virginia and Dignum, Frank and van Harmelen, Frank},
     pages = {630--638},
     publisher = {{IOS} Press},
     series = {Frontiers in Artificial Intelligence and Applications},
     timestamp = {Tue, 02 Nov 2021 15:59:05 +0100},
     title = {Subsumed Label Elimination for Maximum Satisfiability},
     url = {https://doi.org/10.3233/978-1-61499-672-9-630},
     volume = {285},
     year = {2016},
     bdsk-url-1 = {https://doi.org/10.3233/978-1-61499-672-9-630}
   }

3. LMHS: A SAT-IP Hybrid MaxSAT Solver

   Paul Saikko, Jeremias Berg, and Matti Järvisalo

   In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, 2016

   DOI Bib

   @inproceedings{DBLP:conf/sat/SaikkoBJ16,
     author = {Saikko, Paul and Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/sat/SaikkoBJ16.bib},
     booktitle = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
     doi = {10.1007/978-3-319-40970-2\_34},
     editor = {Creignou, Nadia and Berre, Daniel Le},
     pages = {539--546},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     timestamp = {Tue, 14 May 2019 10:00:41 +0200},
     title = {{LMHS:} {A} {SAT-IP} Hybrid MaxSAT Solver},
     url = {https://doi.org/10.1007/978-3-319-40970-2\_34},
     volume = {9710},
     year = {2016},
     bdsk-url-1 = {https://doi.org/10.1007/978-3-319-40970-2%5C_34}
   }

2015

1. Re-using Auxiliary Variables for MaxSAT Preprocessing

   Jeremias Berg, Paul Saikko, and Matti Järvisalo

   In 27th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2015, Vietri sul Mare, Italy, November 9-11, 2015, 2015

   DOI Bib

   @inproceedings{DBLP:conf/ictai/BergSJ15,
     author = {Berg, Jeremias and Saikko, Paul and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ictai/BergSJ15.bib},
     booktitle = {27th {IEEE} International Conference on Tools with Artificial Intelligence, {ICTAI} 2015, Vietri sul Mare, Italy, November 9-11, 2015},
     doi = {10.1109/ICTAI.2015.120},
     pages = {813--820},
     publisher = {{IEEE} Computer Society},
     timestamp = {Fri, 24 Mar 2023 00:04:32 +0100},
     title = {Re-using Auxiliary Variables for MaxSAT Preprocessing},
     url = {https://doi.org/10.1109/ICTAI.2015.120},
     year = {2015},
     bdsk-url-1 = {https://doi.org/10.1109/ICTAI.2015.120}
   }

2. Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT

   Jeremias Berg, Paul Saikko, and Matti Järvisalo

   In Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, 2015

   Bib

   @inproceedings{DBLP:conf/ijcai/BergSJ15,
     author = {Berg, Jeremias and Saikko, Paul and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ijcai/BergSJ15.bib},
     booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, {IJCAI} 2015, Buenos Aires, Argentina, July 25-31, 2015},
     editor = {Yang, Qiang and Wooldridge, Michael J.},
     pages = {239--245},
     publisher = {{AAAI} Press},
     timestamp = {Tue, 20 Aug 2019 16:16:44 +0200},
     title = {Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT},
     url = {http://ijcai.org/Abstract/15/040},
     year = {2015},
     bdsk-url-1 = {http://ijcai.org/Abstract/15/040}
   }

2014

1. Optimal Neighborhood Preserving Visualization by Maximum Satisfiability

   Kerstin Bunte, Matti Järvisalo, Jeremias Berg, and 3 more authors

   In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada, 2014

   DOI Bib

   @inproceedings{DBLP:conf/aaai/BunteJBMPK14,
     author = {Bunte, Kerstin and J{\"{a}}rvisalo, Matti and Berg, Jeremias and Myllym{\"{a}}ki, Petri and Peltonen, Jaakko and Kaski, Samuel},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/aaai/BunteJBMPK14.bib},
     booktitle = {Proceedings of the Twenty-Eighth {AAAI} Conference on Artificial Intelligence, July 27 -31, 2014, Qu{\'{e}}bec City, Qu{\'{e}}bec, Canada},
     doi = {10.1609/AAAI.V28I1.8974},
     editor = {Brodley, Carla E. and Stone, Peter},
     pages = {1694--1700},
     publisher = {{AAAI} Press},
     timestamp = {Mon, 04 Sep 2023 16:50:23 +0200},
     title = {Optimal Neighborhood Preserving Visualization by Maximum Satisfiability},
     url = {https://doi.org/10.1609/aaai.v28i1.8974},
     year = {2014},
     bdsk-url-1 = {https://doi.org/10.1609/aaai.v28i1.8974}
   }

2. Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability

   Jeremias Berg, Matti Järvisalo, and Brandon M. Malone

   In Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, AISTATS 2014, Reykjavik, Iceland, April 22-25, 2014, 2014

   Bib

   @inproceedings{DBLP:conf/aistats/BergJM14,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti and Malone, Brandon M.},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/aistats/BergJM14.bib},
     booktitle = {Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, {AISTATS} 2014, Reykjavik, Iceland, April 22-25, 2014},
     pages = {86--95},
     publisher = {JMLR.org},
     series = {{JMLR} Workshop and Conference Proceedings},
     timestamp = {Wed, 29 May 2019 08:41:44 +0200},
     title = {Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability},
     url = {http://proceedings.mlr.press/v33/berg14.html},
     volume = {33},
     year = {2014},
     bdsk-url-1 = {http://proceedings.mlr.press/v33/berg14.html}
   }

3. SAT-Based Approaches to Treewidth Computation: An Evaluation

   Jeremias Berg, and Matti Järvisalo

   In 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, Limassol, Cyprus, November 10-12, 2014, 2014

   DOI Bib

   @inproceedings{DBLP:conf/ictai/BergJ14,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/ictai/BergJ14.bib},
     booktitle = {26th {IEEE} International Conference on Tools with Artificial Intelligence, {ICTAI} 2014, Limassol, Cyprus, November 10-12, 2014},
     doi = {10.1109/ICTAI.2014.57},
     pages = {328--335},
     publisher = {{IEEE} Computer Society},
     timestamp = {Fri, 24 Mar 2023 00:04:32 +0100},
     title = {SAT-Based Approaches to Treewidth Computation: An Evaluation},
     url = {https://doi.org/10.1109/ICTAI.2014.57},
     year = {2014},
     bdsk-url-1 = {https://doi.org/10.1109/ICTAI.2014.57}
   }

2013

1. Optimal Correlation Clustering via MaxSAT

   Jeremias Berg, and Matti Järvisalo

   In 13th IEEE International Conference on Data Mining Workshops, ICDM Workshops, TX, USA, December 7-10, 2013, 2013

   DOI Bib

   @inproceedings{DBLP:conf/icdm/BergJ13,
     author = {Berg, Jeremias and J{\"{a}}rvisalo, Matti},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/icdm/BergJ13.bib},
     booktitle = {13th {IEEE} International Conference on Data Mining Workshops, {ICDM} Workshops, TX, USA, December 7-10, 2013},
     doi = {10.1109/ICDMW.2013.99},
     editor = {Ding, Wei and Washio, Takashi and Xiong, Hui and Karypis, George and Thuraisingham, Bhavani and Cook, Diane J. and Wu, Xindong},
     pages = {750--757},
     publisher = {{IEEE} Computer Society},
     timestamp = {Fri, 24 Mar 2023 00:01:14 +0100},
     title = {Optimal Correlation Clustering via MaxSAT},
     url = {https://doi.org/10.1109/ICDMW.2013.99},
     year = {2013},
     bdsk-url-1 = {https://doi.org/10.1109/ICDMW.2013.99}
   }