A New Quantum Evolutionary Algorithm with Sifting Strategy for Binary Decision Diagram Ordering Problem

A New Quantum Evolutionary Algorithm with Sifting Strategy for Binary Decision Diagram Ordering Problem

Abdesslem Layeb (University Mentouri of Constantine, Algeria) and Djamel-Eddine Saidouni (University Mentouri of Constantine, Algeria)
DOI: 10.4018/978-1-4666-1743-8.ch016
OnDemand PDF Download:
$37.50

Abstract

In this work, the authors focus on the quantum evolutionary quantum hybridization and its contribution in solving the binary decision diagram ordering problem. Therefore, a problem formulation in terms of quantum representation and evolutionary dynamic borrowing quantum operators are defined. The sifting search strategy is used in order to increase the efficiency of the exploration process, while experiments on a wide range of data sets show the effectiveness of the proposed framework and its ability to achieve good quality solutions. The proposed approach is distinguished by a reduced population size and a reasonable number of iterations to find the best order, thanks to the principles of quantum computing and to the sifting strategy.
Chapter Preview
Top

Introduction

The checking of software and electrical circuit is crucial element to detect the errors which they contain or to show that they function well. One of the most used verification methods used is the model-checking (Clarke, 1994). However, the great difficulty encountered in the domain of formal verification is the combinatorial explosion problem. For example in the model checking, the number of states in the transition graphs can reach prohibitive level, which makes their manipulation difficult or impossible. Consequently, compression methods are used in order to reduce the size of the state graph. The compression is done by using data structures in order to represent in a concise manner the set of states. In this case, the operations are done so on set of states rather than on explicit states.

The representation by the Binary Decision Diagrams BDD is among the most known symbolic notations (Akers, 1978; Drechsler & Becker, 1998). The BDD is a data structure used to efficiently represent Boolean functions. Since they offer a canonical representation and an easy manipulation, the BDD is largely used in several fields such as the logic synthesis (Hachtel & Somenzi, 2006) and the formal verification (Hu, Dill, Drexler, & Yang, 1992). However, the BDD size depends strongly on the selected variable order. Therefore it is important to find a variable order which minimizes the number of nodes in a BDD. The BDD variable order is very important especially in the symbolic model checking, employed in the formal verification of digital circuits and other finite state systems (McMillan, 1992). The exact methods used to resolve this problem are based on dynamic programming with pruning to find the optimal order (Ishiura, Sawada, & Yajima, 1991; Drechsler, Drechsler, & Slobodova, 1998; Friedman & Supowit, 1987). Unfortunately, these methods are not practicable for large instances considering the fact that there are an exponential number of possible variable orders. Indeed, the problem of variable ordering has been shown to be Np-difficult (Bollig & Wegener, 2002). For that, several heuristics were proposed to find the best BDD variable order and which can be classified in two categories. The first class tries to extract the good order by inspecting the logical circuits (Fujii, Ootomo, & Hori, 1988; Fujita, Fujisawa, & Kawato, 1988), whereas, the second class is based on the dynamic optimization of a given order (Meinel & Slobodova, 1997; Ishiura, Sawada, & Yajima, 1991). The Sifting algorithm introduced by Rudell (1993) constitutes one of the most successful algorithms for dynamic reordering of variables. This algorithm is based on finding the best position of a variable in the order by moving the variable to all possible positions while preserving the other variables static. There are other methods based on metaheuristics like genetic algorithms (Drechsler, Becker, & Göckel, 1996; Costa, Déharbe, & Moreira, 2000), simulated annealing (Bollig, Löbbing, & Wegener, 1995), and scatter search algorithm (Hung & Song, 2001).

Complete Chapter List

Search this Book:
Reset