108:30 — Labeling Methods for Partially Ordered Paths

The multi-objective shortest path problem (MOSP) is a well-studied combinatorial optimization problem that has recently seen significant methodological advances. It can easily be reinterpreted as optimizing over a partial order on the paths, namely the d-fold product order of the canonical total order on the real numbers. This raises the question whether labeling methods for MOSP can be generalized to find sets of efficient paths with regard to different partial orders. Previous attempts to answer this question were either limited to acyclic graphs or to specific applications, usually solved with modifications of Martins' algorithm. The structure that these modifications exploit is often closely related but clouded by application-specific language.
In this talk, we formalize the partial order shortest path problem (POSP), introduce generalized labeling methods for POSP and identify properties of POSP instances that guarantee the correctness of these methods. By basing our general label-setting method on the recently introduced Multi-Objective Dijkstra Algorithm, we improve on the best achieved theoretical complexity for all POSP variants that were previously solved using Martins' algorithm without additional effort. Finally, we provide a taxonomy that allows the reader to quickly discern whether their specific application of POSP is suitable for generalized labeling methods and show that several classical shortest path problems fit well within our framework.

209:00 — Measuring Constituency Based On Minimum Campaign Distance And Application To Evaluate The Merger Of Electoral Districts

The area and population of an electoral district are main indicators of its constituency size. They are not, however, indicators that can be used to limit the merger of electoral districts for Japan’s upper house (House of Councilors). This study proposes the minimum campaign distance (MCD) as a new indicator for measuring constituency size and examines relevant issues based on actual measurements, with the aim of using this indicator to evaluate the merger of electoral districts. With characteristics different from those of area and population, the MCD is an indicator that can be used to limit the merger of electoral districts. Here, the campaign duration is evaluated based on the MCD required to cover the entire constituency. Also, the inverse relationship between the number of constituents to cover and the MCD is quantified based on the MCD required to cover a portion of the constituency. The relationship varies across prefectures, which could explain why campaign strategies differ among regions. Lastly, the MCD is used to evaluate the merger of electoral districts: efficiency in terms of travel distance resulting from a merger of electoral districts, the effect of a merger on the smaller district (prefecture), and the feasibility of a merger are formulated as attributes calculated based on the MCD in order to demonstrate a new method of quantitatively evaluating a merger. We also present the result of the computational experiments. Test instances are generated from the Japanese national census.

309:30 — Combinatorial solving with provably correct results

Since the turn of the millennium there have been dramatic improvements in algorithms for combinatorial solving and optimization. The flipside of this is that as solvers get more and more sophisticated, it becomes harder to avoid bugs sneaking in during algorithm design and implementation, and it is well documented that even the most mature tools sometimes return incorrect results. Software testing, while important, has not been sufficient to resolve this problem, and formal verification methods are far from being able to scale to the level of complexity in modern combinatorial solvers. During the last ten years the Boolean satisfiability (SAT) community has instead successfully introduced proof logging, meaning that algorithms have to output, along the answer to a problem, a machine-verifiable proof that this answer is correct, but this success has not been replicated in stronger combinatorial optimization paradigms.

In the last few years, this has started to change with the introduction of so-called pseudo-Boolean proof logging using 0-1 integer linear constraints. In this talk, we will illustrate how this approach seems to hit a sweet spot between simplicity and ease of verification on the one hand and expressive power on the other. We will try to provide a glimpse how pseudo-Boolean reasoning has enabled proof logging not only for previously unsupported advanced SAT techniques (including symmetry breaking) but also for SAT-based optimization (MaxSAT solving), subgraph solving, constraint programming, and most recently presolving techniques in 0-1 integer linear programming (ILP). Perhaps the most striking feature of this method is that proofs can be written in a simple proof format referred to as "cutting planes with strengthening rules" that knows nothing about symmetries, groups, graphs, integer-valued variables, or global constraints.

410:00 — On the monotonicity in steepest descent algorithm for M-convex functions

M-convex function is a class of discrete convex function defined on the integer lattice points, and plays a primary role in the theory of discrete convex analysis. We consider the minimization of an M-convex function. It is known that a minimizer of an M-convex function can be found by a steepest descent algorithm in a finite number of iterations. In this talk, we present some monotonicity properties of the steepest descent algorithm for the class of M-convex functions and a more general class of discrete convex functions called jump M-convex functions. We show that the algorithm finds the “nearest” optimal solution to a given initial solution. We also analyze the trajectory of the solutions generated by the algorithm, and show that it is a "shortest” path from the initial solution to the “nearest” optimal solution. We also invesitage the monotonicity in the slope of steepest descent directions.