Added the Oct/Nov sessions (#3)

* Added the Oct/Nov sessions
* Uploaded the bibliography entries

_bibliography/s20241014.bib

@@ -0,0 +1,58 @@
+@ARTICLE{Ihalainen2024-jArtifIntellRes,
+  title     = "Unifying {SAT}-based approaches to maximum satisfiability solving",
+  html = "https://www.jair.org/index.php/jair/article/view/15986",
+  author    = "Ihalainen, Hannes and Berg, Jeremias and J{\"{a}}rvisalo, Matti",
+  journal   = "The journal of artificial intelligence research",
+  publisher = "AI Access Foundation",
+  volume    =  80,
+  pages     = "931--976",
+  abstract  = "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.",
+  month     =  "7~" # jul,
+  year      =  2024,
+  keywords  = "automated reasoning; combinatorial optimization; Boolean
+               satisfiability;MaxSAT;Propositional satisfiability",
+  doi       = "10.1613/jair.1.15986",
+  language  = "en"
+}

_bibliography/s20241104.bib

@@ -0,0 +1,64 @@
+@ARTICLE{ZattoniScroccaro2024-operRes,
+  title     = "Learning in Inverse Optimization: Incenter Cost, Augmented
+               Suboptimality Loss, and Algorithms",
+  html = "https://pubsonline.informs.org/doi/abs/10.1287/opre.2023.0254",
+  author    = "Zattoni Scroccaro, Pedro and Atasoy, Bilge and Mohajerin
+               Esfahani, Peyman",
+  journal   = "Operations research",
+  publisher = "Institute for Operations Research and the Management Sciences
+               (INFORMS)",
+  abstract  = "Enhancing the Efficiency and Accuracy of Inverse Optimization
+               Inverse optimization (IO) is used to model the behavior of
+               decision-making agents who solve optimization problems in
+               response to external signals. Inspired by the geometry of IO
+               problems, in ``Learning in Inverse Optimization: Incenter Cost,
+               Augmented Suboptimality Loss, and Algorithms,'' Zattoni
+               Scroccaro, Atasoy, and Mohajerin Esfahani propose the
+               ``incenter'' concept to solve IO problems, which unlike
+               previously proposed approaches, can be used to derive
+               computationally tractable solutions to this modeling problem.
+               Moreover, they also propose a novel loss function for IO problems
+               and a tailored optimization algorithm to optimize it. Extensive
+               numerical experiments showcase the improved efficiency and
+               accuracy of the proposed IO formulations and algorithm.",
+  year      =  2024,
+  keywords  = "Predict-and-optimize;Inverse optimization",
+  doi       = "10.1287/opre.2023.0254",
+  language  = "en"
+}
+
+@ARTICLE{ZattoniScroccaro2024-transpSci,
+  title     = "Inverse optimization for routing problems",
+  html = "https://pubsonline.informs.org/doi/abs/10.1287/trsc.2023.0241",
+  author    = "Zattoni Scroccaro, Pedro and van Beek, Piet and Mohajerin
+               Esfahani, Peyman and Atasoy, Bilge",
+  journal   = "Transportation science",
+  publisher = "Institute for Operations Research and the Management Sciences
+               (INFORMS)",
+  abstract  = "We propose a method for learning decision makers' behavior in
+               routing problems using inverse optimization (IO). The IO
+               framework falls into the supervised learning category and builds
+               on the premise that the target behavior is an optimizer of an
+               unknown cost function. This cost function is to be learned
+               through historical data, and in the context of routing problems,
+               can be interpreted as the routing preferences of the decision
+               makers. In this view, the main contributions of this study are to
+               propose an IO methodology with a hypothesis function, loss
+               function, and stochastic first-order algorithm tailored to
+               routing problems. We further test our IO approach in the Amazon
+               Last Mile Routing Research Challenge, where the goal is to learn
+               models that replicate the routing preferences of human drivers,
+               using thousands of real-world routing examples. Our final
+               IO-learned routing model achieves a score that ranks second
+               compared with the 48 models that qualified for the final round of
+               the challenge. Our examples and results showcase the flexibility
+               and real-world potential of the proposed IO methodology to learn
+               from decision-makers' decisions in routing problems. History:
+               This paper has been accepted for the Transportation Science
+               Special Issue on TSL Conference 2023. Funding: This work was
+               supported by the European Research Council [TRUST-949796].",
+  year      =  2024,
+  keywords  = "VRP;Inverse optimization",
+  doi       = "10.1287/trsc.2023.0241",
+  language  = "en"
+}

_bibliography/s20241125.bib

@@ -0,0 +1,40 @@
+@ARTICLE{Schreiber2024-jArtifIntellRes,
+  title     = "{MallobSat}: Scalable {SAT} solving by clause sharing",
+  html = "https://www.jair.org/index.php/jair/article/view/15827",
+  author    = "Schreiber, Dominik and Sanders, Peter",
+  journal   = "The journal of artificial intelligence research",
+  publisher = "AI Access Foundation",
+  volume    =  80,
+  pages     = "1437--1495",
+  abstract  = "SAT solving in large distributed environments has previously led
+               to some famous results and to impressive speedups for selected
+               inputs. However, in terms of general-purpose SAT solving, prior
+               approaches still cannot make efficient use of a large number of
+               processors. We aim to address this issue with a complete and
+               systematic overhaul of the distributed solver HordeSat with a
+               focus on its algorithmic building blocks. In particular, we
+               present a communication-efficient approach to clause sharing,
+               careful buffering and filtering of produced clauses, and
+               effective orchestration of state-of-the-art solver backends. In
+               extensive evaluations, our approach named MallobSat significantly
+               outperforms an updated HordeSat, doubling its mean speedup. Our
+               clause sharing results in effective parallelization even if all
+               threads execute identical solver programs that only differ based
+               on which clauses they import at which times. We thus argue that
+               MallobSat is not a portfolio solver with the added bonus of
+               clause sharing but rather a clause-sharing solver where adding
+               some explicit diversification is useful but not essential. We
+               also discuss the last four iterations of the International SAT
+               Competition (2020--2023), where our system ranked very favorably,
+               and identify several previously unsolved competition problems
+               that MallobSat solved successfully. Last but not least, our
+               approach is malleable, i.e., supports running on a fluctuating
+               set of resources, which allows us to combine parallel job
+               processing and parallel SAT solving in a flexible manner for best
+               resource efficiency",
+  month     =  "18~" # aug,
+  year      =  2024,
+  keywords  = "automated reasoning; satisfiability;Propositional satisfiability",
+  doi       = "10.1613/jair.1.15827",
+  language  = "en"
+}

_sessions/2024-10-14-unifying-maxsat.md

@@ -0,0 +1,11 @@
+---
+layout: session
+title: "Unifying SAT-Based Approaches to Maximum Satisfiability Solving"
+host: Imko Marijnissen
+session_type: paper
+related_papers: s20241014
+---
+
+In this talk I will discuss the paper "Unifying SAT-Based Approaches to Maximum Satisfiability Solving"; the paper explores the differences between the 3 different approaches to MaxSAT (core-guided search, implicit hitting sets and objective bounding) and to what extent they are different.
+
+Each of the 3 aforementioned approaches has its strengths and weaknesses but it is poorly understood in what sense they fundamentally differ and how they could potentially be combined. To this end, the paper proposes a new framework, UniMaxSAT, for unifying these approaches and shows that all 3 approaches can be simulated using this framework. Additionally, the paper shows that this framework can be used to create new variants of the 3 approaches.

_sessions/2024-11-04-invopt.md

@@ -0,0 +1,9 @@
+---
+layout: session
+title: "Inverse Optimization"
+host: Pedro Zattoni Scroccaro
+session_type: research
+related_papers: s20241104
+---
+
+In Inverse Optimization problems, a learning agent aims to learn how to mimic the behavior of an expert agent, which given an exogenous signal, returns an action. The underlying assumption is that in order to compute its action, the expert agent solves an optimization problem parametric in the exogenous signal. Therefore, given examples of exogenous signals and corresponding expert actions, the goal of the learner is to learn the cost function being optimized by the expert. In this presentation, we will talk about fundamental concepts of Inverse Optimization and novel results, as well as applications to static and dynamic routing problems.

_sessions/2024-11-18-column-elimination.md

@@ -0,0 +1,9 @@
+---
+layout: session
+title: "Column Elimination: An Iterative Approach to Solving Integer Programs"
+host: Anthony Karahalios
+host_ref: https://amkarahalios.github.io/
+session_type: research
+---
+
+Column elimination is an exact algorithm to solve discrete optimization problems via a 'column' formulation in which variables represent a combinatorial structure such as a machine schedule or truck route. Column elimination works with a relaxed set of columns, from which infeasible ones are iteratively eliminated. As the total number of columns can typically be exponentially large, we use relaxed decision diagrams to compactly represent and manipulate the set of columns. In this talk, we provide an introduction to the column elimination method and present recent algorithmic improvements resulting in competitive performance on large-scale vehicle routing problems. Specifically, our approach closes a large vehicle routing benchmark instance with 1,000 locations for the first time.

_sessions/2024-11-25-mallobsat.md

@@ -0,0 +1,9 @@
+---
+layout: session
+title: "Column Elimination: An Iterative Approach to Solving Integer Programs"
+host: Maarten Flippo
+host_ref: https://maartenflippo.com
+session_type: paper
+---
+
+During this MOO session I will present a paper on using parallel computing to solve large-scale SAT problems. One of the typical ways to exploit parallel computing is to run a portfolio solver, essentially trying many different configurations to race. In this work, however, a method is presented which works well even when all threads run identical configurations.