Circuit-width based heuristic for Boolean reasoning

Binary decision diagram (BDD) and Boolean satisfiability (SAT) are two common techniques of logic circuit-based Boolean reasoning. Since circuit-width is a good measure of circuit complexity, in this paper, a circuit-width based heuristic for Boolean reasoning is presented, it can be used for integrating the BDD-based engine and SAT-based engine, and takes advantages of both engines. Thus this heuristic can avoid the potential memory explosion during constructing the BDDs, and can prevent the time-out phenomenon of SAT techniques. Compared with the previous heuristics, the proposed heuristic can save more computational resources, and can improve the performance of Boolean reasoning algorithms. This heuristic has been applied in combinational circuit test generation successfully. Experimental results show that, the proposed heuristic can be used for the Boolean reasoning with multiple engines efficiently.