EVBDD-based algorithms for integer linear programming, spectral transformation, and function decomposition

Edge-Valued Binary-Decision Diagrams (EVBDD´s) are directed acyclic graphs that can represent and manipulate integer functions as effectively as Ordered Binary-Decision Diagrams OBDD´s) do for Boolean functions. They have been used in logic verification for showing the equivalence between Boolean functions and arithmetic functions. In this paper, we present EVBDD-based algorithms for solving integer linear programs, computing spectral coefficients of Boolean functions, and performing function decomposition. These algorithms have been implemented in C under the SIS environment and experimental results are provided