School of Computing

An Anytime Symmetry Detection Algorithm for ROBDDs

Neil Kettle and Andy King

In Hidetoshi Onodera, editor, Eleventh Asia and South Pacific Design Automation Conference, pages 182-196. IEEE, January 2006 Copyright held by IEEE 2006.

Abstract

Detecting symmetries is crucial to logic synthesis, technology mapping, detecting function equivalence under unknown input correspondence, and ROBDD minimization. State-of-the-art is represented by Mishchenko's algorithm. In this paper we present an efficient anytime algorithm for detecting symmetries in Boolean functions represented as ROBDDs, that output pairs of symmetric variables until a prescribed time bound is exceeded. The algorithm is complete in that given sufficient time it is guaranteed to find all symmetric pairs. The complexity of this algorithm is in O(n^4+n|G|+|G|^3) where n is the number of variables and |G| the number of nodes in the ROBDD, and it is thus competitive with Mishchenko's |G|^3 algorithm in the worst-case since n << |G|. However, our algorithm performs significantly better because the anytime approach only requires lightweight data structure support and it offers unique opportunities for optimization.

Download publication 234 kbytes (PostScript)

Bibtex Record

@inproceedings{2253,
author = {Neil Kettle and Andy King},
title = {An {A}nytime {S}ymmetry {D}etection {A}lgorithm for {ROBDD}s},
month = {January},
year = {2006},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Copyright held by IEEE 2006.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2006/2253},
    publication_type = {inproceedings},
    submission_id = {231_1128085680},
    booktitle = {Eleventh Asia and South Pacific Design Automation Conference},
    editor = {Hidetoshi Onodera},
    publisher = {IEEE},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014