A method, system and computer program product are disclosed. The method includes initializing a first variable to limit a rewrite time for rewrite operations with respect to an initial design by a rewriting module, a second variable to limit a time for satisfiability solver operations with respect to said initial design by a satisfiability solver module and a third variable to limit a maximum number of rewrite iterations with respect to said initial design. A timer is called to track said rewrite time and a local logic rewriting operation is run on said initial design with said rewrite module. In response to determining that all of all targets for said initial design netlist are not solved, whether a rewrite time is expired is determined. In response to determining that said rewrite time is not expired, AND refactoring is run. In response to determining that said rewrite time is not expired, XOR refactoring is run.