A SAT-Based Exact Approach for the Minimum Order Frequency Assignment Problem

Abstract

The Minimum Order Frequency Assignment Problem (MO-FAP) is a fundamental NP-hard problem in spectrum management, where the objective is to minimize the number of assigned frequencies while satisfying interference constraints between transmitters. Current metaheuristic methods typically do not provide optimality certificates, while traditional exact methods can struggle on heavily constrained instances. This study proposes an exact framework based on Boolean Satisfiability (SAT) for solving MO-FAP. The key idea is to use standard order variables to reformulate pairwise interference constraints as interval-boundary constraints in a proposed encoding called POSE, thereby reducing the number of explicit conflict clauses relative to a direct SAT encoding. In addition, the framework includes an incremental SAT solving strategy (INCSC) based on Sequential Counter encoding, where the clause construction is designed to support incremental solving and clause reuse across iterations without rebuilding the formula. Experiments on 35 CALMA and DUTtest benchmark instances from the FAP database show that the proposed approach certifies optimality or infeasibility for every tested instance within a 600-second time limit. On the tested benchmark set, it certifies more instances than the considered exact baselines and reduces solving time on several instances where the baselines reach the time limit. These results show that the proposed SAT-based framework provides exact certification with competitive runtime on the tested MO-FAP benchmark instances.