A theoretical analysis of the conditions under which LBBD, including cuts, can preserve optimality in the context of Answer Set Programming (ASP), a prominent logic-based language in the field of Artificial Intelligence and introduces a general-purpose algorithm that preserves the optimality guarantees of Bender Decomposition.
We present an open-source software package that implements a provably convergent Benders-type decomposition algorithm for multistage stochastic integer programs. In addition to standard cut families, such as Benders, strengthened Benders, and Lagrangian cuts, the algorithm incorporates rectified linear unit (ReLU) cuts, which provide convergence guarantees for general mixed-integer state variables. However, the dual problems used to generate these cuts often admit multiple optimal solutions. Although each solution yields a valid cut that separates the incumbent, the resulting cuts can differ in how well they approximate the subproblem cost. To strengthen these cuts, our package implements and evaluates two cut-selection strategies based on normalization and regularization of the dual problem. We also incorporate an alternating-cut criterion that uses cheaper Benders cuts when they are effective and invokes more expensive tight cuts only when necessary. Computational experiments on four classes of multistage stochastic integer programs benchmark these methods and provide insights on how problem structure affects their practical performance.
It is proved that Minimal-to-Maximal Conversion Search is in fact not output-polynomial and the lower bound construction motivates a more detailed analysis of how certain heuristic choices in the algorithm design affect the running time.
This work introduces a framework that addresses both verification levels in the Lean theorem prover, and can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families.
Pablo Manrique, Stefan Szeider· arXiv.org· 0 citations
