Bisect-Index-Choose: A Fast and Exact Algorithm for EV Charging under Minimum Charging Rates
Can Berk Saner
eess.SY
Nov 7, 2026 · v1
TL;DR
The paper's theorems and lemmas on the BIC algorithm's optimality are formalized in Lean 4, with the formalization released in a public repository.
Abstract
Electric vehicle (EV) charging stations are increasingly operated with an aggregate power limit below the sum of their port ratings, and require scheduling algorithms to divide the available power among the connected EVs. Charging standards permit a current that is either zero or at least a minimum rate, typically 6 A, which makes this allocation problem non-convex. Existing methods either solve a mixed-integer program with a commercial solver, which can be computationally expensive, adds software dependencies, and incurs licensing costs, or apply heuristics without optimality guarantees. This paper proposes Bisect-Index-Choose (BIC), a fast and solver-free scheduling algorithm that computes a globally optimal allocation among EVs under mild assumptions on their utilities. For $n$ EVs, BIC runs in $O(n \log n)$ time when all EVs share one maximum rate and in $O(n^2)$ time for two, times a logarithmic factor in the numerical precision. In tests with up to 1000 EVs, BIC attains global optimality and is up to three orders of magnitude faster than the solver. On real-world charging data, it needs less capacity and delivers more energy than existing heuristics. We implement BIC on a low-cost microcontroller and show that it solves instances with 1000 EVs in less than 90 ms.
Problem
EV charging stations with an aggregate power cap must split power among connected EVs. Charging standards require each current to be either zero or at least a minimum rate, which makes the allocation non-convex. Existing approaches either rely on commercial mixed-integer solvers or use heuristics with no optimality guarantee.
Approach
Bisect-Index-Choose (BIC) dualizes the budget constraint using a generalized Lagrange multiplier method and bisects on the multiplier. It then resolves the discontinuities of the aggregate rate function (Everett gaps) by indexing EVs in priority order and choosing the best candidate allocation. Global optimality is proven under mild assumptions on the utilities, and these theorems and lemmas are formalized in Lean 4.
Results
BIC runs in O(n log n) time for one maximum rate and O(n^2) for two, and attains global optimality on all 815 synthetic instances, where the heuristics fall to 0% and 33% of optimal utility. It is up to three orders of magnitude faster than a MIP solver and solves 1000-EV instances in under 90 ms on a microcontroller.