An exact input encoding algorithm for BDDs representing FSMs

We address the problem of encoding the state variables of a finite state machine such that the BDD representing its characteristic function has the minimum number of nodes. We present an exact formulation of the problem. Our formulation characterizes the two BDD reduction rules by deriving conditions under which these reduction rules can be applied. We then provide an algorithm that finds these conditions and solves the problem by formulating it as a 2-CNF formula and extracting all its prime implicants. In addition to this, we implemented a simulated annealing algorithm for this problem and provide a thorough experiment of the impact of encoding on a BDD representing an FSM with different orderings