Compact SAT encoding for power peak minimization in assembly line balancing

Abstract

The Simple Assembly Line Balancing Problem with Power Peak Minimization (SALB3PM) minimizes maximum instantaneous power usage while assigning n tasks to m workstations and determining execution schedules within given cycle time constraints. This NP-hard problem couples workstation assignment, temporal sequencing, and power aggregation, presenting significant computational challenges for exact optimization methods. Existing Boolean Satisfiability (SAT) and Maximum Satisfiability (MaxSAT) approaches rely on pairwise station and time encodings that can generate quadratic numbers of clauses in the workstation or cycle-time dimensions. We introduce a Compact SAT Encoding (CSE) using sequential counter techniques to reduce assignment, scheduling, and precedence encodings from pairwise to linear-size formulations in these dimensions. We instantiate four optimization variants over the resulting CSE model: clause-blocking SAT refinement, pseudo-Boolean bound tightening, MaxSAT, and ordered peak-indicator incremental SAT. Comprehensive experimental evaluation on benchmark instances demonstrates consistent performance improvements over state-of-the-art approaches, including higher coverage and lower cumulative solving time under the standard timeout. The encoding principles generalize to other assembly line balancing variants and broader scheduling problems with precedence constraints.