1. A method for designing circuits, the method comprising: providing, using a microprocessor, a first quantified conjunctive normal form formula; determining dependency sequents for the left branch and the right branch of a branching variable; determining whether both branches of the branching variable are unsatisfied; and designing a circuit using a current formula having less variables than the first quantified conjunctive normal formula.