PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Huy Tuan Nguyen, Duc Trung Kim Nguyen, Khanh To Van

arXiv:2608.25351v1cs.LO

TL;DR

The JSPPR adds time-varying instantaneous power limits to job shop scheduling, but prior work lacked exact SAT and constraint-programming approaches. This paper develops both formulations and shows that each proves optimality for all 35 benchmark instances, with identical optimal makespans and CP requiring less computational effort than SAT.

  • Problem

    Prior JSPPR research was limited to a MILP formulation and a GRASP × ELS metaheuristic despite the need to enforce time-varying instantaneous power limits.

  • Method

    The paper develops exact SAT and CP formulations using order and pseudo-Boolean encodings for SAT and interval variables and global constraints for CP.

  • Results

    35 benchmark instances achieve proven optimality with identical optimal makespans under both SAT and CP, while CP consistently requires less computational effort than SAT.

  • Takeaways & Limitations

    The independently verified optimal results provide a reliable reference for future studies of the JSPPR benchmark.

  • Takeaways & Limitations

    The available JSPPR benchmarks are relatively small, so these results do not establish whether exact SAT and CP remain competitive with metaheuristics on larger problems.

Abstract

from arXiv · show

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.

1. Introduction

The JSPPR extends classical job shop scheduling with operation power requirements and time-dependent limits on instantaneous total power. This paper addresses the resulting gap by introducing exact SAT and CP approaches and evaluating them on all 35 published benchmark instances.

  • Introduction: JSPPR schedules must satisfy precedence and machine-capacity constraints while keeping total power demand below the available threshold at every time.Exceeding power limits may cause financial penalties, equipment overload, or grid instability.
  • Introduction: The JSPPR couples otherwise independent operations because simultaneous execution can violate the time-dependent upper bound on combined power consumption.Each operation has a power requirement, making instantaneous power a constraint in addition to classical scheduling requirements.
  • Introduction: The paper develops the first SAT-based JSPPR approach with order-based start-time encoding and pseudo-Boolean power constraints, alongside a CP model using interval variables and global constraints.The CP formulation reformulates the earlier MILP model.
  • Introduction: 35 published JSPPR instances were evaluated, with both SAT and CP proving global optimality for all instances and establishing four new bounds beyond GRASP × ELS.CP is substantially faster at proving optimality.

2. JSPPR: Problem Definition and Related Work

JSPPR extends job shop scheduling with operation-level power requirements and time-varying instantaneous power limits, while minimizing makespan under precedence, machine-capacity, continuity, and power constraints. Although CP and SAT have shown promise for exact classical JSSP solving, JSPPR had lacked such formulations despite existing MILP and metaheuristic approaches.

  • Problem Definition: JSPPR assigns each operation a power requirement and imposes a time-dependent limit on total instantaneous consumption while minimizing feasible-schedule makespan.Schedules must satisfy precedence, machine capacity, continuity, and power constraints.
  • Problem Definition: Each job follows a predetermined route across machines, with fixed-duration, non-preemptive operations whose peak-power and nominal-power phases proceed consecutively.The jobs, routes, machines, and processing requirements are known before scheduling.
  • Illustrative Example: The illustrative 2 × 2 instance achieves optimal makespan Cmax = 187 under the time-varying power threshold.The schedule completes both final operations at t = 186 and t = 187 before the maintenance blackout at t = 196.
  • Related Work: CP and SAT have demonstrated competitive exact-solving performance for classical JSSP, including scalable CP models and compact SAT encodings.The cited work motivates extending both paradigms to scheduling problems with additional resource constraints.
  • Research Gap: JSPPR literature had mathematical programming and metaheuristic approaches but no SAT or CP exact formulations, which this paper addresses with both formulations.The CP formulation is derived from the existing MILP model, while the SAT formulation is introduced for JSPPR.

3. Preprocessing for Exact Approaches

The exact approaches first require an instance-specific feasible makespan upper bound because time-varying power thresholds make simple total-processing-time bounds insufficient. This bound defines the scheduling horizon, which supports start-time domain reduction and the SAT and CP formulations.

  • A finite upper bound is essential because it defines the scheduling horizon and restricts variable domains and search space, while total processing time is insufficient under time-varying power limits.
  • A randomized greedy heuristic repeatedly selects an unscheduled job uniformly at random and assigns its next operation to the earliest feasible start time satisfying precedence, machine-capacity, and power constraints.The procedure abandons infeasible constructions and repeats within a fixed time limit, retaining the best feasible schedule as UB.
  • The horizon derived from the best schedule found is subsequently used for start-time domain reduction and both exact formulations.Algorithm 1 summarizes the randomized greedy upper-bound computation.
  • For each operation op_j,i, preprocessing computes earliest and latest feasible starts from job precedence and horizon H, excluding machine-capacity and power constraints.Assuming all jobs are available at time 0, ES_j,0 = 0; subsequent bounds follow sequential job processing, while LS_j,i = H − rem_j,i.
  • Each operation receives the reduced domain [ES_j,i, LS_j,i]; if ES_j,i > LS_j,i, the instance is deemed infeasible under H and model construction is skipped.Otherwise, the reduced domains restrict start-time variables in both CP and SAT formulations.

4. Constraint Programming Formulation

The CP formulation reformulates the MILP scheduling relationships and resource constraints with interval variables and global constraints. It models operations, job and machine interactions, and time-varying power limits within a makespan-minimization model.

  • Model structure: The formulation derives from the MILP model by representing scheduling relationships and resource constraints with CP interval variables and global constraints.This preserves the underlying problem structure while representing temporal and resource interactions with CP-specific constructs.
  • Operation representation: Each operation uses a mandatory master interval with fixed length P_j,i and a start-time domain restricted to [ES_j,i, LS_j,i].The start-time bounds are obtained during preprocessing.
  • Power representation: Operation power consumption is modeled through mandatory phase intervals for peak and nominal phases, with zero-duration phases omitted.The peak phase has duration a_j,i and power W_j,i + W′_j,i; the nominal phase has duration P_j,i − a_j,i and power W_j,i.
  • Scheduling constraints: Job precedence is enforced by ordering operations within each job, while a global no-overlap constraint prevents operations assigned to the same machine from overlapping.Redundant non-consecutive precedence constraints can improve propagation and reduce the search space.
  • Power-limit enforcement: A time-varying power threshold is converted into a constant-limit cumulative constraint by adding fixed dummy intervals that reserve unusable power in each horizon segment.The standard cumulative constraint cannot directly represent the piecewise-constant threshold profile; dummy intervals leave exactly PT_q available during segment q.
  • Objective: The model minimizes C_max, defined as the completion time of the last operation, subject to constraints (CP-1)–(CP-7).This objective captures the scheduling makespan.

5. SAT Formulation

The SAT formulation models JSPPR schedules over a discrete-time horizon, encoding start times, precedence, machine capacity, and time-dependent power constraints. It separates feasible-schedule encoding from incremental makespan optimization, using progressively tighter bounds until unsatisfiability certifies optimality.

  • 5.1. Encoding Variables and Constraints: Each operation uses Boolean start-time variables within a reduced feasible domain, from which execution phases and scheduling constraints are derived.The reduced domain is [ES_o, LS_o], and variables are introduced only for start times remaining possible after preprocessing.
  • 5.2. Incremental Optimization: Incremental optimization retains one persistent CDCL solver state while appending decreasing makespan bounds, terminating with a provably optimal incumbent when the next bound is unsatisfiable.The two-stage procedure first constructs a base encoding of feasible schedules, then tightens makespan bounds without recreating formulas or discarding learned clauses.
  • 5.1. Encoding Variables and Constraints: Order variables X_o,t encode starts at or after t, while exact-start variables S_o,t identify the unique transition corresponding to each operation’s start time.Monotonicity and boundary conditions ensure exactly one start time is selected in each reduced domain.
  • 5.1. Encoding Variables and Constraints: Precedence clauses require each successor to start no earlier than its predecessor’s completion, including rules that exclude starts extending beyond the horizon.For consecutive operations, a predecessor starting at t imposes a successor start at least t + p_j,i.
  • 5.1. Encoding Variables and Constraints: Symmetric machine-exclusion clauses forbid overlapping execution intervals for every pair of distinct operations assigned to the same machine.The cumulative representation excludes the overlapping window [t−p_o′ +1, t+p_o−1].
  • 5.1. Encoding Variables and Constraints: Peak and nominal phase variables derive each operation’s power consumption, and candidate sets restrict each time-indexed power constraint to phases that may cover that instant.Peak consumption occupies the first a_o instants, while nominal consumption occupies the remaining p_o−a_o instants.
  • 5.1. Encoding Variables and Constraints: Binary Merger encoding converts the weighted pseudo-Boolean power constraints into equivalent CNF clauses for SAT solving.The base encoding jointly specifies operation start times, execution phases, precedence, machine non-overlap, and power feasibility.
  • 5.3. Complexity Analysis: Under worst-case reduced-domain size D_o = O(H), each operation’s feasible start-time domain scales linearly with the scheduling horizon H.D_o = |[ES_o, LS_o]| = LS_o−ES_o+1, and the complexity section states that the SAT encoding size is analyzed under D_o = O(H).

6. Computational Experiments

Across 35 JSPPR benchmark instances, SAT and CPLEX CP proved optimality for every instance and achieved the best-known makespan on all instances. CPLEX CP was faster, while exact methods improved or corrected several previously reported results.

  • Aggregate performance: 35 instances: SAT and CPLEX CP each achieved #OPTIMAL = 35 and #BEST = 35, while GRASP × ELS achieved the best makespan on 24 instances.GRASP × ELS does not provide optimality certificates.
  • Aggregate performance: 263.12 seconds: CPLEX CP’s cumulative proof time was lower than SAT’s 2,672.55 seconds.Both methods achieved the same solution quality and optimality coverage; CPLEX CP was approximately an order of magnitude faster.
  • Solution quality: 4 new optimal makespan values: SAT and CPLEX CP improved solutions reported by the GRASP × ELS metaheuristic.For JSPPR 2 10x4, the optimum was 6 units lower than previously reported; for JSPPR 4 10x4, it was reduced by 23 units from 680.
  • Benchmark re-evaluation: 49 units: discrepancies separated some historical GRASP × ELS makespans from verified optimal values across seven benchmark instances.SAT and CPLEX CP obtained identical makespan values while solving all instances to proven optimality, so lower historical values require cautious interpretation.
  • Scaling behavior: 25 seconds: CPLEX CP’s proof times remained below this threshold for 10-job instances, whereas SAT reached 871.49 seconds on JSPPR 4 10x4.For instances with 4–6 jobs, both methods proved optimality within seconds; SAT proved all instances optimal within the 3,600-second limit.

7. Conclusion

The paper introduces exact SAT and constraint programming approaches for JSPPR and evaluates them on 35 benchmark instances. Both approaches prove optimality for every instance, while CP requires less computational effort than SAT and the results provide reliable baselines for future studies.

  • Contributions: The study develops two exact approaches for JSPPR based on SAT solving and constraint programming, extending prior work limited to MILP and GRASP × ELS.JSPPR adds an instantaneous power-consumption limit to the classical job shop scheduling problem.
  • Computational evaluation: 35 benchmark instances: SAT and CP prove optimality for all instances and obtain identical optimal makespans.Both exact approaches demonstrate stronger optimality-solving performance than MILP.
  • Computational evaluation: CP consistently requires less computational effort than SAT across the evaluated JSPPR benchmark instances.The re-evaluation also identified inconsistencies in several previously reported GRASP × ELS makespans, which were excluded from comparison.
  • Limitations and future work: The currently available JSPPR benchmark instances are relatively small, leaving the scalability of exact SAT and CP approaches on larger problems unresolved.The independently verified results provide reliable exact baselines for future evaluations on larger and more diverse instances.

CRediT authorship contribution statement

The authors contributed across methodology, analysis, software, validation, investigation, visualization, writing, supervision, project administration, conceptualization, and data curation.

  • Huy Tuan Nguyen handled methodology, software, validation, investigation, data curation, visualization, and writing—review and editing.
  • Duc Trung Kim Nguyen contributed conceptualization, methodology, formal analysis, visualization, original-draft writing, and review and editing.
  • Khanh To Van contributed investigation, conceptualization, methodology, formal analysis, supervision, project administration, and review and editing.

Funding details

The authors received no specific grant funding for this research.

  • Funding details: No specific grant supported the research from public, commercial, or not-for-profit funding agencies.

Declaration on the use of generative AI

The authors used OpenAI ChatGPT (GPT-5.6) for language refinement and consistency checks, while reviewing and verifying all outputs and retaining responsibility for the manuscript’s content.

  • Declaration on the use of generative AI: The authors used OpenAI ChatGPT (GPT-5.6) for language refinement and consistency checks, then reviewed and verified all outputs.They retain full responsibility for the accuracy, originality, citations, analyses, and conclusions.

Appendix A. Benchmark Validation and Inconsistency Analysis · A.1. Invalid Machine References in the Benchmark Instances · A.2. Infeasible Reported Schedules Due to Power Constraint Violations

The appendix validates the benchmark data and reported schedules, identifying invalid machine references and power-constraint violations that undermine some published results. It documents parsing and verification procedures supporting consistent reconstruction and independent feasibility checks.

  • A.1. Invalid Machine References in the Benchmark Instances: All instances define four machines, indexed 0–3, so machine-dependent blocks should contain exactly four machine-value pairs.The benchmark files nevertheless include undeclared machine references in affected instances.
  • A.1. Invalid Machine References in the Benchmark Instances: 10 instances contain an additional reference to machine 4, which is not among the four machines declared in the input.The same inconsistency is identified across the instances listed in Table A1.
  • A.1. Invalid Machine References in the Benchmark Instances: JSPPR 3 4x4 illustrates the defect with five machine-value pairs despite a four-machine header.Its nominal-power line includes (4, 16), referring to a fifth machine absent from the instance.
  • A.1. Invalid Machine References in the Benchmark Instances: Undeclared machine-value pairs were ignored during parsing to retain four valid pairs and reconstruct affected benchmark data consistently.This treatment supports reproduction but does not remove the original input error.
  • A.2. Infeasible Reported Schedules Due to Power Constraint Violations: Reported schedules were independently checked by taking published start times and machine assignments as given, then recomputing total power over the scheduling horizon.At each time point t, active-operation power requirements were summed according to the reported assignments and execution data.
  • A.2. Infeasible Reported Schedules Due to Power Constraint Violations: 9 benchmark instances contain reported schedules whose recomputed power exceeds the allowed threshold at one or more time points.Among them, 7 have reported makespan values strictly smaller than the optimal values established in this study.
Loading 2608.25351v1…