salle A. Turing CE4
22 March 2013 - 14h00
Saucy3: Fast Symmetry Discovery in Graphs
by Karem Sakalla from University of Michigan Ann Arbor
Abstract: In this talk I will describe the saucy symmetry detection algorithm. The origins of Saucy can be traced to our attempt to find and break the symmetries of difficult SAT instances. A CNF instance was encoded as a colored graph and passed on to a graph automorphism tool to find a set of symmetry generators (vertex permutations that preserve the edge relation) which were then used to create symmetry-breaking predicates for the CNF formula. At the time, existing graph automorphism tools were unable to handle the large sparse graphs that encode CNF instances and saucy 1.0 was created to address that need. Since that time, Saucy underwent significant algorithmic change, motivated by the parallel between searching for permutations that are symmetries of a graph and searching for satisfying assignments to a formula by a SAT solver. Saucy3 is currently the fastest and most scalable graph automorphism program and has been applied to problems in a wide range of domains.
Karem A. Sakallah received the B.E. degree in electrical engineering from the American University of Beirut in 1975, and the M.S. and Ph.D. degrees in electrical and computer engineering from Carnegie Mellon University, Pittsburgh, PA, in 1977 and 1981, respectively. Since 1988, he has been with the University of Michigan, Ann Arbor, as a Professor of Electrical Engineering and Computer Science His current research interests include the area of computer-aided design of electronic systems, Boolean satisfiability, discrete optimization, and hardware and software verification. In 2009 he was a co-recipient of the prestigious Computer Aided Verification Award for fundamental contributions to the development of high-performance Boolean satisfiability solvers. His research in satisfiability and hardware verification led to the creation in 2009 of a start-up company, Reveal Design Automation, which he co-founded with two of his doctoral students.
