Abstract
In the presentation he will introduce a method of how SAT can be used for finding maybe smaller data structures of circuits. At the moment ordered binary decision diagrams (or BDD's for short) are a common data structure with many advantages (canonical, 100% testable, etc.) but some disadvantages, too (i.e. memory explosion). For finding smaller decision diagrams (to avoid memory explosion) it could help to discard the restriction of ordering and trying to build unordered - so called free - binary decision diagrams (or FBDD's for short). For this SAT could be very helpful as SAT-solver exploring the search-space in a way, we could use for FBDD-construction. Because of the well optimized heuristics and algorithms we may be able to constructed better, that means smaller, FBDD's. Besides an introduction and motivation Robert will describe first approaches, discuss the results and introduce some planned improvements.
Biography
Robert Wille is student of computer science at the University of Bremen (Germany) since 2002. At the moment he is writing his diploma thesis (akin to master) and work on some projects at the Group of Computer Architecture in Bremen headed by Prof. Dr. Rolf Drechsler. His main research interests are on SAT and SAT-related topics.