Reducing interpolant circuit size through SAT-based weakening