Nowadays, designers of digital logic circuits are looking for getting as maximum accuracy as possible for the designed circuits with possible minimum consumed time, and finally with as minimum effort as possible. Overcoming all of these constraints cannot be achieved by traditional approaches even when using Karnaugh-Maps, especially when using more than 4-input variables. The most important problem facing the designers is selecting which and how the optimum solution(s) are possible, taking into consideration the order of variables to decide how many equivalent digital logic circuits can be extracted from the original one. This book depends on the Binary Decision Diagram approach to be used to represent in symbolic manner a set of input-variables. It is largely used in the field of formal checking. The variable ordering is a very important step in the Binary Decision Diagram optimization process. A good order of variables will reduce considerably the size of a Binary Decision Diagram. We hope you will enjoy reading the fruit of our efforts and that this book will help you to obtain a general perspective on Binary Decision Diagrams.