Boolean Matrix Factorization with SAT and MaxSAT
This work addresses matrix approximation for data analysis, but it is incremental as it builds on existing factorization methods with specific algorithmic improvements.
The paper tackles the Boolean matrix factorization problem by proposing SAT and MaxSAT encodings for small matrices and a heuristic based on maximal biclique edge cover for large matrices, achieving better factorization than existing approaches with reasonable computation times and handling incomplete matrices.
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.