arXiv subjects

Duc Trung Kim Nguyen

Publications and source records attributed to Duc Trung Kim Nguyen.

3 recordsLinked to original sources

arXiv2026

Exact SAT and Constraint Programming for Job Shop Scheduling with Time-Varying Peak Power Constraints

The Job Shop Scheduling Problem with Power Requirements (JSPPR) extends the classical job shop scheduling problem by imposing time-varying limits on instantaneous power consumption. Previous studies have used a mixed-integer linear programming formulation and the GRASP x ELS metaheuristic, but no SAT-based exact approach or constraint programming model has been reported. This paper develops the first exact SAT and constraint programming (CP) formulations for the JSPPR. On the 35 published benchmark instances, both SAT and CP prove global optimality for all instances and obtain identical optimal makespans, substantially improving upon the best previously reported results. They also establish four improved makespan values over the GRASP x ELS results reported in the original study. CP proves optimality faster than SAT, while both exact approaches substantially improve the optimality coverage of the MILP formulations, which prove optimality on only 6 and 10 instances using CPLEX and Gurobi, respectively. The certified optimal solutions also reveal inconsistencies in several previously reported benchmark results, including makespans below the proven optimum. We provide corrected optimal makespans and a complete set of certified optimal results for the JSPPR benchmark, establishing a reliable reference for future studies.

cs.LO↗

arXiv2026

Proving Optimality for the Bandwidth Multicoloring Problem via SAT

The Bandwidth Multicoloring Problem (BMCP) is an NP-hard extension of the Bandwidth Coloring Problem (BCP) with important applications in telecommunications, resource allocation, and scheduling. While state-of-the-art metaheuristics can efficiently produce high-quality solutions, they cannot certify global optimality. Existing exact approaches based on Constraint Programming (CP) and Integer Programming (IP) provide such guarantees but typically require extensive computation and still lag behind metaheuristics in solution quality, leaving many benchmark instances without optimality certificates. In this paper, we present the first SAT-based exact framework for the BMCP. Our main contribution is an efficient SAT encoding that compactly models both intra-vertex and inter-vertex color distance constraints. Combined with tight color domain reduction and an incremental SAT-solving strategy, the proposed formulation significantly prunes the search space and enables efficient exact optimization. Experimental results on the GEOM and MS-CAP benchmark suites demonstrate substantial improvements over previous exact approaches. On the challenging GEOM benchmark, the proposed framework proves optimality for more instances within only one hour of computation than the previous CP/IP approach, which required a 48-hour time limit, while also verifying the optimality of several previously reported best-known solutions. These results demonstrate that SAT-based reasoning provides an effective exact optimization framework for the BMCP and substantially expands the range of benchmark instances whose optimality can be certified.

cs.LO↗

arXiv2026

SAT Encodings for Bandwidth Coloring: A Systematic Design Study

The Bandwidth Coloring Problem (BCP) generalizes graph coloring by enforcing minimum separation constraints between adjacent vertices and arises in frequency assignment applications. While SAT-based approaches have shown promise for exact BCP solving, the encoding design space remains largely unexplored. This paper presents a systematic study of SAT encodings for the BCP, proposing a unified framework with six encoding methods across three categories: one-variable, two-variable, and block encodings. We evaluate the impact of key features including incremental solving and symmetry breaking. While symmetry breaking has been studied for graph coloring, it has not been systematically evaluated for SAT-based BCP solvers. Our analysis reveals significant interaction effects between encoding choices and solver configurations. The proposed framework achieves state-of-the-art performance on GEOM and MS-CAP benchmarks. Block encodings solve GEOM120b, the hardest instance, to proven optimality in approximately 1000 seconds, whereas previous methods could not solve it within a one-hour time limit.

cs.LO↗