Accelerating Discrete Facility Layout Optimization: A Hybrid CDCL and CP-SAT Architecture

Technical Summary: Conflict-Driven Clause Learning with VSIDS Heuristics for Discrete Facility Layout

Problem Definition
The paper addresses the Discrete Facility Layout Problem (FLP), specifically focusing on grid-based layouts where machines must be assigned to slots under dense combinatorial constraints. These constraints include one-to-one assignment, adjacency requirements (must-be-neighbors), separation constraints (forbidden neighbors), blocked cells (aisles), and multi-floor slotting. While canonical formulations often treat FLP as a Quadratic Assignment Problem (QAP), real-world instances introduce logic-heavy constraints that create a dense combinatorial structure. The study investigates whether modern SAT solvers utilizing Conflict-Driven Clause Learning (CDCL) with the Variable State Independent Decaying Sum (VSIDS) heuristic can effectively exploit this structure, and under what conditions they compare favorably against established Constraint Programming (CP-SAT) and Mixed-Integer Linear Programming (MILP) approaches.

Methodology
The authors developed a unified benchmarking harness in Python to conduct controlled comparisons across three solver paradigms:

1. CDCL+VSIDS: Implemented using PySAT with Glucose4 and MiniSat22 back-ends. The layout feasibility is encoded in Conjunctive Normal Form (CNF) using Boolean variables ($z_{ij}$) for machine-slot assignments. Constraints are encoded via cardinality constraints (using sequential counters or totalizers to reduce clause count), adjacency/separation clauses, and unit clauses for blocked cells. Optimization is handled by treating CDCL as a feasibility engine, while optimization objectives are addressed via hybrid architectures.
2. CP-SAT: Implemented via Google OR-Tools, leveraging global constraints and pseudo-Boolean reasoning.
3. MILP: Implemented via PuLP with CBC, utilizing linearized QAP formulations.

Experimental Design
The study utilized synthetic data to isolate algorithmic performance from real-world variance. Experiments varied across:

• Grid Sizes: Ranging from 2×2 to 6×6 (with 5×5 serving as a threshold for MILP failure and 6×6 as a limit test for intractability).
• Constraint Density ($\rho$): Varied from 0.05 to 0.35.
• Structural Types: Assignment-only, adjacency-constrained, separation-constrained, and mixed.
• Symmetry: Tests were run with and without positional fixing of the first machine to break symmetry.
• Timeouts: 10 seconds for feasibility checks and 60 seconds for optimization trials.

Key Findings

• Feasibility Detection: CDCL+VSIDS demonstrates near-constant runtime performance across varying grid sizes and constraint densities, outperforming CP-SAT by one to two orders of magnitude and MILP by even larger margins. CDCL excels at pruning the search space for pure feasibility.
• Optimization: While CDCL is rapid at finding a solution, it cannot natively optimize soft objectives (like minimizing Manhattan distance) without MaxSAT or iterative bound tightening, which adds overhead. CP-SAT excels at hybrid logical-numerical optimization, proving global optima for 5×5 and 6×6 instances where MILP failed to converge within the time limit.
• MILP Limitations: MILP exhibits exponential slowdown as grid size and constraint density increase, struggling with the weak linear relaxations caused by big-M disjunctions and dense pairwise terms.
• Symmetry Breaking: Fixing a machine's position significantly improved CP-SAT (27%) and MILP (50%) runtimes but caused a slight slowdown for CDCL, as the added clauses increased formula complexity without providing the same pruning benefits in a clause-learning context.

Hybrid Architectures
To leverage the speed of CDCL and the optimization quality of CP-SAT, the authors proposed two hybrid architectures:

1. Deep Enumeration (Architecture A): CDCL enumerates a large pool of feasible layouts (75,000 samples), and CP-SAT selects the best. This approach found a viable solution (Obj=22.0) in ~24 seconds, significantly faster than the 60-second CP-SAT baseline, though it did not reach the global optimum (Obj=13.0).
2. Warm-Start (Architecture B): CDCL generates a single rapid feasible hint (an upper bound) and injects it into CP-SAT's branch-and-bound process. This approach achieved the global optimum (Obj=13.0) with a validated runtime advantage over the cold-start baseline, demonstrating that CDCL-driven hints effectively prune the initial branches of the search tree.

Significance and Claims
The paper claims that the most effective path for discrete facility layout optimization is not to replace exact solvers but to accelerate them using CDCL-driven feasibility hints. The study establishes that:

• CDCL+VSIDS possesses "unrivaled dominance" in pure feasibility detection for logic-heavy, grid-based FLPs, solving complex adjacency and separation rules orders of magnitude faster than CP-SAT or MILP.
• Pure CDCL struggles with cost-aware optimization, making it unsuitable as a standalone optimizer for these problems.
• Hybrid architectures, specifically the Warm-Start approach, successfully bridge the gap between rapid satisfiability and proven optimality. By using CDCL to provide a valid upper bound, the hybrid system achieves global optima with validated algorithmic speed advantages over cold-start baselines.

The authors conclude that while CDCL is rarely applied to full-scale factory FLPs due to optimization mismatches and encoding overheads, its integration as a feasibility engine within a hybrid framework offers a robust solution for high-complexity layout problems.