New research shows that open Boolean satisfiability (SAT) solvers can out-compute two of the biggest names in commercial optimization software on a classic graph-labeling puzzle.
Antibandwidth problems ask you to number the nodes of a graph so that connected nodes get labels as far apart in value as possible. Most prior work chased that "maximize the gap" version. This paper flips it: fix how far apart connected labels must be, then find the smallest range of numbers needed to pull it off. The authors call this the Minimum Span Antibandwidth problem, plus a cyclic variant, and solve both with a SAT-based framework that works through a sequence of decision problems, either checking several candidate ranges at once or narrowing one search step by step. Tested on benchmark matrices from the Harwell-Boeing collection, the SAT methods matched or beat CPLEX and Gurobi - the default commercial tools for this kind of optimization - and won outright on the cyclic version.
That result matters beyond the math department. CPLEX and Gurobi are the go-to engines for hard scheduling, layout, and resource-allocation problems across engineering and logistics, and they aren't free. Watching a SAT-based approach - built on much older, more accessible logic techniques - hold its own or win against them suggests exact optimization still has room for cheaper alternatives to catch up.
Don't expect this in a product roadmap. It's a benchmark study on a fairly obscure labeling problem, and the practical payoff, if any, is years out.