Shrink the Range, Keep the Distance

TL;DR for operators

If every conflicting pair in an allocation system must already be separated by at least $k$ units, the unresolved question is often not how far apart assignments can be pushed. It is how little total capacity is required to satisfy that rule.

Hieu Truong Xuan and Khanh To Van formalize that question as Minimum Span Antibandwidth Labeling and Minimum Span Cyclic Antibandwidth Labeling.¹ For a fixed separation requirement, feasibility moves monotonically with the candidate label-domain size: once a candidate range is large enough, every larger one is feasible as well. That structure lets an exact solver treat capacity as an ordered sequence of feasibility tests rather than a generic optimization variable.

The implementation consequence is more interesting than the terminology. Multiple candidate spans can be tested in parallel and discarded as soon as the feasible-infeasible boundary moves. For the ordinary linear-distance problem, the solver can also tighten the domain incrementally while retaining learned SAT clauses. The cyclic version cannot use that construction directly because changing the domain size changes the cyclic distances themselves.

On the paper’s base benchmark, incremental SAT solved all 120 linear instances, proved 112 optimal, and returned a best-known span on all 120. Parallel SAT solved all 120 cyclic instances, proved 107 optimal, and returned 116 best-known spans. The stronger no-hole restriction produces less decisive comparisons with CPLEX constraint programming, so these results support a structural solver choice under the tested conditions rather than a general claim that SAT always wins.

The variable to minimize is capacity

Suppose a frequency-assignment or scheduling system contains pairs that cannot be placed too close together. The minimum separation $k$ is fixed by interference, safety, timing, or another operational constraint. Once that requirement is non-negotiable, maximizing separation is no longer the natural objective. The operator instead wants the smallest resource range that can still accommodate every assignment.

That reverses the conventional antibandwidth formulation. Standard antibandwidth fixes the available label domain and asks how large the minimum separation can become. The paper fixes the required separation and minimizes the span.

If $f$ assigns integer labels to vertices, the realized span is

For the linear problem, adjacent vertices must satisfy

The cyclic variant measures the shorter distance around a label cycle:

That final $\lambda$ matters later. It is not merely a bound on available labels; it participates directly in the cyclic constraint.

Monotone feasibility turns optimization into ordered search

For fixed $k$, candidate capacity has a one-directional property. If a labeling is feasible with largest label $\lambda$, it remains feasible when the allowed domain is enlarged. Conversely, an infeasible candidate implies that every smaller candidate is also infeasible.

This converts minimum-span optimization into a boundary search. A SAT solver does not need to solve every possible $\lambda$ independently. A feasible result tightens the upper boundary; an infeasible result raises the lower boundary.

The paper’s parallel strategy exploits this ordering by testing several candidate spans concurrently. When one process establishes a new feasible or infeasible boundary, searches that can no longer improve the answer can be terminated.

For architects of exact allocation systems, the transferable point is not specifically graph labeling. When a capacity parameter produces monotone feasibility, parallel capacity testing can use information from one candidate to eliminate other candidates before they finish. The affected decision is how to allocate solver processes across candidate capacities; the condition is that feasibility genuinely preserves this ordering.

Incremental reuse works only when tightening preserves semantics

The linear formulation has another structural advantage. Reducing $\lambda$ removes labels from the domain, but it does not change the distance between labels that remain.

That allows the MSABL solver to build a SAT instance at an upper bound, progressively forbid labels as the candidate span decreases, and retain clauses learned during earlier solves. Nearby capacity tests therefore share solver state instead of starting from zero.

It is tempting to assume the cyclic problem should admit the same optimization. It does not.

In MSCABL, cyclic distance contains $\lambda$ directly. Reducing the label domain changes the wrap-around distance even between labels that were already present. The new problem is therefore not simply the previous problem plus a few forbidden labels. Existing constraints have changed meaning.

This is a useful implementation boundary for systems beyond this benchmark: incremental optimization is safe when tightening a resource domain removes options while leaving the semantics of retained options unchanged. If the resource limit itself appears inside the constraint function, reusing solver state requires additional justification.

The base benchmark favors the SAT formulations

The authors evaluate 24 Harwell-Boeing graphs, split into 12 small and 12 large instances, and scale the prescribed separation across five coefficients. This produces 120 MSABL and 120 MSCABL base-model instances. Competing methods operate under a common 1,800-second time limit, 45 GB memory limit, and access to up to eight concurrent processes where applicable.

The paired Wilcoxon comparisons reinforce the aggregate pattern. For MSABL, both SAT approaches outperform CPLEX_CP overall at conventional significance levels, although the difference between parallel and incremental SAT is not significant at $0.05$ ($p=0.0633$). For MSCABL, parallel SAT significantly outperforms CPLEX_CP, CPLEX_MIP, and Gurobi in the overall comparisons.

These experiments support the SAT design on this benchmark and resource regime. They do not establish that SAT is the generally superior technology for every minimum-capacity allocation problem.

The no-hole test shows where the advantage becomes less stable

The paper also evaluates a stronger restriction: every label between 1 and the realized maximum must be used. This is best read as a robustness or formulation-sensitivity test rather than a second main thesis.

Under this no-hole condition, results become more mixed. For MSABL, parallel and incremental SAT prove 36 and 35 optimal solutions, respectively, compared with 33 for CPLEX_CP. Yet CPLEX_CP solves 59 of the 72 instances, versus 54 for parallel SAT and 52 for incremental SAT, and has the best overall average rank. The overall SAT-versus-CPLEX_CP differences are not statistically significant.

MSCABL shows a similar trade-off. Parallel SAT obtains 42 optimal and 57 best-known solutions versus 38 and 48 for CPLEX_CP, but CPLEX_CP solves more instances, 66 versus 57. Their overall Wilcoxon difference is not statistically significant ($p=0.1171$).

The practical conclusion therefore sits below the level of solver branding. The paper provides strong evidence that its SAT formulations exploit the structure of the base problems effectively. Once the formulation is strengthened, the comparative advantage over CPLEX_CP is less consistent.

For allocation systems, model semantics determine solver architecture

Cognaptus inference: the paper is most relevant to operators whose separation requirement is fixed before optimization begins. Spectrum-like assignment, constrained scheduling, and related resource-allocation systems can then express the planning question as the smallest feasible capacity rather than the largest achievable separation.

For engineering teams, two checks follow.

First, determine whether feasibility is monotone in the capacity parameter. If it is, candidate capacities can be searched as an ordered boundary and parallel resources can be concentrated around that boundary.

Second, determine what happens when capacity shrinks. If tightening merely removes options, incremental solver reuse may preserve valuable learned information. If tightening changes the meaning of constraints among options that remain—as it does for cyclic distance here—the solver architecture must account for that semantic change rather than assuming reuse is valid.

What remains uncertain is how far the reported performance carries beyond the 24 Harwell-Boeing graphs, the paper’s coefficient construction, solver implementations, hardware configuration, and resource limits. The authors also identify room to reduce SAT formula size, strengthen propagation, improve symmetry breaking, and adapt span or resource allocation dynamically.

The durable contribution is narrower and more useful: when the service requirement is fixed, capacity itself can become the optimization target, and the algebra of that capacity parameter determines which exact-solving strategies can safely exploit repeated work.

Cognaptus: Automate the Present, Incubate the Future.