Exact minimization of binary decision diagrams using implicit techniques