Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Certified Inductive Synthesis for Online Mixed-Integer Optimization

Marco Zamponi, Emilio Incerto, Daniele Masti, Mirco Tribastone

TL;DR

The paper tackles online mixed-integer optimization by combining counterexample-guided inductive synthesis (CEGIS) with an offline-online decomposition. It constructs a certified, piecewise-constant predictor $\Delta^{\ast}$ that maps problem parameters to feasible binary decisions, enabling online solutions to fix binaries and solve only the continuous subproblem. The approach yields substantial real-time speedups while maintaining feasibility guarantees, demonstrated on two CPS-inspired benchmarks; however, the offline verification and synthesis steps face scalability and termination challenges, particularly due to NRA quantifier handling. Future work aims to reduce predictor complexity, enhance suboptimality performance, and extend the framework to larger, higher-dimensional problems with improved verifiers and synthesis strategies.

Abstract

In fields such as autonomous and safety-critical systems, online optimization plays a crucial role in control and decision-making processes, often requiring the integration of continuous and discrete variables. These tasks are frequently modeled as mixed-integer programming (MIP) problems, where feedback data are incorporated as parameters. However, solving MIPs within strict time constraints is challenging due to their $\mathcal{NP}$-complete nature. A promising solution to this challenge involves leveraging the largely invariant structure of these problems to perform most computations offline, thus enabling efficient online solving even on platforms with limited hardware capabilities. In this paper we present a novel implementation of this strategy that uses counterexample-guided inductive synthesis to split the MIP solution process into two stages. In the offline phase, we construct a mapping that provides feasible assignments for binary variables based on parameter values within a specified range. In the online phase, we solve the remaining continuous part of the problem by fixing the binary variables to the values predicted by this mapping. Our numerical evaluation demonstrates the efficiency and solution quality of this approach compared to standard mixed-integer solvers, highlighting its potential for real-time applications in resource-constrained environments.

Certified Inductive Synthesis for Online Mixed-Integer Optimization

TL;DR

The paper tackles online mixed-integer optimization by combining counterexample-guided inductive synthesis (CEGIS) with an offline-online decomposition. It constructs a certified, piecewise-constant predictor that maps problem parameters to feasible binary decisions, enabling online solutions to fix binaries and solve only the continuous subproblem. The approach yields substantial real-time speedups while maintaining feasibility guarantees, demonstrated on two CPS-inspired benchmarks; however, the offline verification and synthesis steps face scalability and termination challenges, particularly due to NRA quantifier handling. Future work aims to reduce predictor complexity, enhance suboptimality performance, and extend the framework to larger, higher-dimensional problems with improved verifiers and synthesis strategies.

Abstract

In fields such as autonomous and safety-critical systems, online optimization plays a crucial role in control and decision-making processes, often requiring the integration of continuous and discrete variables. These tasks are frequently modeled as mixed-integer programming (MIP) problems, where feedback data are incorporated as parameters. However, solving MIPs within strict time constraints is challenging due to their -complete nature. A promising solution to this challenge involves leveraging the largely invariant structure of these problems to perform most computations offline, thus enabling efficient online solving even on platforms with limited hardware capabilities. In this paper we present a novel implementation of this strategy that uses counterexample-guided inductive synthesis to split the MIP solution process into two stages. In the offline phase, we construct a mapping that provides feasible assignments for binary variables based on parameter values within a specified range. In the online phase, we solve the remaining continuous part of the problem by fixing the binary variables to the values predicted by this mapping. Our numerical evaluation demonstrates the efficiency and solution quality of this approach compared to standard mixed-integer solvers, highlighting its potential for real-time applications in resource-constrained environments.

Paper Structure

This paper contains 22 sections, 27 equations, 5 figures, 6 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Running example
  4. Optimal Control Problem
  5. Methodology
  6. Offline Phase
  7. Function Structure
  8. Function Verification
  9. Function Synthesis
  10. Online Phase
  11. Function Evaluation
  12. Online Problem Solution
  13. Experiments
  14. Methodology Implementation
  15. Nonlinear Controller Obstacle Avoidance
  16. ...and 7 more sections

Figures (5)

  • Figure 1: Overview of the proposed two-phase methodology for solving online optimization problems. (a) During the offline phase, a function between real-time parameter realizations and feasible binary variable assignments is synthesized through a CEGIS procedure. This phase is computationally expensive and is executed offline; thus, it does not impact operations during the system execution. (b) In the online phase, the pre-computed map is used to quickly compute feasible values for binary variables, while the remaining continuous decision variables are computed by numerical solvers in real time.
  • Figure 2: Example iterative verification and refinement process for synthesizing the piecewise function $\Delta^{\ast}$. (a) The verification of the domain $\Omega$ (filled in gray) results in the identification of a counterexample (marked as a big cross). (b) Points from the domain $\Omega$ are randomly sampled for refinement (marked as dots and crosses depending on their optimal binary assignment). (c) The domain $\Omega$ is split into two subdomains $\Omega^{(1)}$ and $\Omega^{(2)}$, forming new branches of the piecewise function.
  • Figure 3: Domain partition for the nonlinear obstacle avoidance problem: the black area represents the infeasible region occupied by the rectangular obstacle, while the remaining states are divided into four feasible regions.
  • Figure 4: Solving times in the nonlinear system benchmark for optimization problems: \ref{['eq:mpMIP']}, on y-axis and \ref{['eq:mpMIP_deltafixed']}, with binary variables predicted by $\Delta^{\ast}$ on x-axis.
  • Figure 5: Solving times in the inertial system benchmark for optimization problems: (\ref{['eq:mpMIP']}), on y-axis and (\ref{['eq:mpMIP_deltafixed']}), with binary variables predicted by $\Delta^{\ast}$ on x-axis.