Factorization using binary decision diagrams