|
Fadi A. Aloul, Ph.D.
Assistant Professor of Computer Engineering,
American University of Sharjah
Abstract:
The last few years have seen an increasing interest in the Boolean Satisfiability (SAT) problem which is concerned with identifying a variable assignment for a given Boolean formula, expressed in product-of-sums form, that evaluates the formula to true, or proving that no such assignment exists and that the formula is false. Recently, several powerful SAT solvers have been proposed, many of which are able to deal with large-scale SAT problem instances. This has led to the successful deployment of SAT technology into diverse electronic design automation (EDA) applications such as routing, verification, testing, and physical design. Nevertheless, a number of practical SAT instances remain difficult to solve and continue to defy even the best available SAT solvers. While the general SAT problem is NP-complete, we observe that SAT instances arising from real-world applications possess an innate structure that, once uncovered, can drastically simplify the instance. Motivated by this observation, we develop robust methods for detecting various structural properties of hard SAT instances and show how to utilize these properties to produce SAT algorithms that can scale with the increasing complexity of today’s SAT instances.
In this talk, we introduce the Boolean satisfiability problem and describe the commonly used algorithmic approaches for solving SAT. We also highlight the use of SAT in solving a number of EDA problems. In addition, we present completely automated techniques for exploiting symmetries in SAT instances and show how to effectively use such property to substantially speed up the search process.
Biography:
Fadi Aloul received the B.S. degree in electrical engineering summa cum laude from Lawrence Technological University (LTU), and the M.S. and Ph.D. degrees in computer science and engineering from the University of Michigan, Ann Arbor, respectively. He was a post-doc research fellow at the University of Michigan during summer 2003. He was a visiting researcher with the Advanced Technology Group at Synopsys during summer 2005. He is currently an Assistant Professor of Computer Engineering at the American University of Sharjah, UAE.
Prof. Aloul has received a number of awards including the Agere/SRC research fellowship, GANN fellowship, and the LTU presidential scholarship. He served on the technical program committees at the International Workshop on Logic Synthesis (IWLS), the International Conference on Theory and Applications of Satisfiability Testing (SAT), the SIGDA Ph.D. Forum at the Design Automation Conference (DAC), the International Workshop on Soft Constraints (CP-Soft), the International Symposium on Wireless Systems and Networks (ISWSN), and the Innovations in Information Technology Conference (IIT). He was a local organizer of the 2006 IEEE International Conference on Computer Systems and Applications (AICCSA) and the AV chair of the 2003 International Workshop on Logic Synthesis (IWLS). He is a member of the Institute of Electrical and Electronics Engineers (IEEE), Associate of Computing Machinery (ACM), and Tau Beta Pi. Prof. Aloul has 45+ publications in international journals, conferences, and workshops. He has presented several invited talks and tutorials at Intel, Microsoft Research Labs and other EDA companies. He developed several tools used in the SAT and BDD domains, such as the 0-1 ILP SAT solver and optimizer, PBS. His current research interests are in the areas of design automation, combinatorial optimization, Boolean satisfiability, and computer security.
Thursday, January 18th at 3 p.m.
Bossone 303
|
