1. A method of ordering input variables in a binary decision diagram (BDD) representing a Boolean function, comprising: performing a search within said Boolean function for a first and second sub-equations with first and second disjoint sets of said input variables; and building an order of said input variables based on said disjoint sets.