SYMMETRY-DETECTION AND BREAKING FOR BOOLEAN SATISFIABILITY

April 20, 2005
2:50 pm - 4:00 pm
Halligan 108
Speaker: Fadi A Aloul, American University of Sharjah
Host: Soha Hassoun

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.