Boolean Matrix Factorization with SAT and MaxSAT
  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.
