Bi-decomposing large Boolean functions via interpolation and satisfiability solving