Binary Matrix Factorization (BMF) approximates a binary matrix as the Boolean product of two lower-rank binary matrices, providing interpretable patterns for data mining and machine learning. Computing optimal solutions is NP-hard, and existing exact methods face severe scalability limitations. We introduce the first Benders decomposition framework for rank-k Boolean matrix approximation, exploiting problem separability through independent, analytically solvable subproblems—one per matrix entry—that generate cuts by dual inspection, enabling massive parallelization without iterative LP solvers.

Given a binary data matrix X ∈ {0,1}^{n×m} and rank parameter k, the problem seeks binary factor matrices C and R minimizing the Frobenius norm. Our Benders decomposition partitions variables into master variables (C,R) and subproblem variables (z,y). The master problem minimizes an upper bound on reconstruction error, while subproblems decompose additively over entries. For each entry, we solve independent dual subproblems analytically by inspection, generating cuts that enforce Boolean reconstruction consistency.

We apply methods to select Pareto-optimal cuts maximizing separation depth from a core point in the master feasible region. We integrate seven categories of valid inequalities: symmetry-breaking, rank aggregation, biclique constraints, and problem-specific sparsity bounds. Separation employs a hierarchical strategy: valid inequalities are checked first, with Benders separation only when no valid inequalities are violated, yielding 30-50% reduction in cut generation overhead and 20-40% improvement in lower bound quality.

Computational experiments on synthetic (30×30, 50×50, 80×80) and real-world datasets (Mushroom, Votes, Tic-Tac-Toe from UCI) demonstrate consistent superiority over column generation: 0-20% improvement in objective value, 5-30% reduction in solution time, and tighter lower bounds. The method scales to instances an order of magnitude larger (up to 250×250 matrices) than previously tractable. We present the first exact Benders decomposition framework for binary matrix factorization, combining theoretical rigor with practical optimizations.