Compact SAT Encoding for Power Peak Minimization

TL;DR

This paper presents a compact SAT encoding for the Power Peak Minimization problem in assembly line balancing, significantly improving computational efficiency and enabling exact solutions for large industrial instances.

Contribution

The authors introduce a novel compact SAT encoding that reduces clause complexity and demonstrate its effectiveness across multiple optimization variants and large-scale benchmarks.

Findings

Achieves O(m) clauses per precedence edge, improving over previous O(m^2) encodings.

Enables exact optimization on industrial-scale instances previously considered intractable.

Demonstrates consistent performance improvements over existing methods.

Abstract

The Simple Assembly Line Balancing Problem with Power Peak Minimization (SALBP-3PM) 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 suffer from baseline encodings generating $O(m^2)$ clauses per precedence edge. We introduce a Compact SAT Encoding (CSE) achieving $O(m)$ clauses per transitive precedence edge using sequential counter techniques. We instantiate four optimization variants: Clause-Based iterative SAT, Pseudo-Boolean (PB) Constraint iterative SAT, MaxSAT, and Incremental SAT. Comprehensive experimental evaluation on benchmark instances demonstrates consistent performance improvements over state-of-the-art approaches, enabling exact optimization on previously intractable industrial-scale instances. The encoding principles generalize to other assembly line balancing variants and broader scheduling problems with precedence constraints.