Boolean Matrix Factorization with SAT and MaxSAT

TL;DR

This paper introduces SAT and MaxSAT encodings for Boolean matrix factorization, offering improved solutions for small matrices and heuristics for larger ones, including handling incomplete data.

Contribution

It presents novel SAT and MaxSAT formulations for Boolean matrix factorization and a heuristic for large matrices, enhancing accuracy and efficiency.

Findings

Better factorization accuracy than existing methods

Effective handling of incomplete matrices

Reasonable computation times for practical use

Abstract

The Boolean matrix factorization problem consists in approximating a matrix by the Boolean product of two smaller Boolean matrices. To obtain optimal solutions when the matrices to be factorized are small, we propose SAT and MaxSAT encoding; however, when the matrices to be factorized are large, we propose a heuristic based on the search for maximal biclique edge cover. We experimentally demonstrate that our approaches allow a better factorization than existing approaches while keeping reasonable computation times. Our methods also allow the handling of incomplete matrices with missing entries.