Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compact SAT Encoding for Power Peak Minimization

Tuyen Van Kieu, Phong Chi Nguyen, Bao Gia Hoang, Khanh Van To

TL;DR

This paper tackles SALBP-3PM, a scheduling problem that minimizes peak power while assigning tasks to workstations under precedence constraints. It introduces a Compact SAT Encoding (CSE) based on sequential counters and extended precedence preprocessing to reduce per-edge clause complexity from $O(m^2)$ to $O(m)$, and it unifies four optimization variants (Clause-Based, PB, MaxSAT, Incremental SAT) for fair comparison. Empirical results on 89 benchmark instances show substantial improvements over state-of-the-art encodings, with the Incremental SAT variant delivering the best overall performance and solving hard/extreme-hard instances previously out of reach. The approach generalizes to other SALBP variants and broader precedence-constrained scheduling problems, offering a practical path to exact optimization in industrial-scale settings.

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.

Compact SAT Encoding for Power Peak Minimization

TL;DR

This paper tackles SALBP-3PM, a scheduling problem that minimizes peak power while assigning tasks to workstations under precedence constraints. It introduces a Compact SAT Encoding (CSE) based on sequential counters and extended precedence preprocessing to reduce per-edge clause complexity from to , and it unifies four optimization variants (Clause-Based, PB, MaxSAT, Incremental SAT) for fair comparison. Empirical results on 89 benchmark instances show substantial improvements over state-of-the-art encodings, with the Incremental SAT variant delivering the best overall performance and solving hard/extreme-hard instances previously out of reach. The approach generalizes to other SALBP variants and broader precedence-constrained scheduling problems, offering a practical path to exact optimization in industrial-scale settings.

Abstract

The Simple Assembly Line Balancing Problem with Power Peak Minimization (SALBP-3PM) minimizes maximum instantaneous power usage while assigning tasks to 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 clauses per precedence edge. We introduce a Compact SAT Encoding (CSE) achieving 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.

Paper Structure

This paper contains 34 sections, 16 equations, 3 figures, 6 tables, 6 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Problem Definition
  4. Related Work and Background
  5. Related Work
  6. Existing SAT and MaxSAT Encodings
  7. SAT-based Iterative Framework
  8. MaxSAT-based Direct Optimization
  9. Motivation for Compact Encoding
  10. Compact SAT Encoding and Optimization Approaches
  11. Compact Precedence Encoding
  12. Variable Definitions
  13. Constraint Formulation
  14. Complexity Analysis
  15. Extended Precedence Graph Preprocessing
  16. ...and 19 more sections

Figures (3)

  • Figure 1: Illustrative example of SALBP-3PM with 5 tasks distributed across 3 workstations over a cycle time of 7 units
  • Figure 2: Encoding size comparison across 45 commonly-solved instances. Top: total variables (millions); Bottom: total clauses (millions). Solid blue bars represent ORG (baseline encoding); hatched red bars represent CSE (compact encoding)
  • Figure 3: Solving times (seconds, log scale) for 10 hard instances. Timeout (3600s) shown for unsolved cases. Instance abbreviations: B=BUXEY, G=GUNTHER, H=HESKIA, S=SAWYER, W=WARNECKE