Boolean function bi-decomposition is a fundamental operation in logic synthesis. A function f(X) is bi-decomposable under a variable partition Variable partition $$X_A, X_B, X_C$$ on X if it can be written as $$h(f_A(X_A,X_C), f_B(X_B,X_C))$$ for some functions h, f A , and f B . The quality of a bi-decomposition is mainly determined by its variable partition. Variable partition A preferred decomposition is disjoint, i.e., $$X_C = \emptyset$$ , and balanced, i.e., $$|X_A| \approx |X_B|$$ . Finding such a good decomposition reduces communication and circuit complexity and yields simple physical design solutions. Prior BDD-based methods may not be scalable to decompose large functions due to the memory explosion problem. Also as decomposability is checked under a fixed variable partition, Variable partition searching a good or feasible partition may run through costly enumeration that requires separate and independent decomposability checkings. This chapter proposes a solution to these difficulties using interpolation and incremental SAT solving SAT!incremental . Preliminary experimental results show that the capacity of bi-decomposition can be scaled up substantially to handle large designs.