| Description |
Boolean Satisfiability: From Theoretical Hardness to Practical Success
With Sharad Malik
Chair, Department of Electrical Engineering
Princeton University
Refreshments will be served outside Room 339 at 3:45 p.m.
Faculty Host: Ajay Joshi
Abstract: Boolean Satisfiability (SAT) is the problem of checking if a propositional logic formula can ever evaluate to true. This problem has long enjoyed a special status in computer science. On the theoretical side, it was the first problem to be classified as being NP-complete. On the practical side, SAT manifests itself in several important application domains such as the design and verification of hardware and software systems, as well as applications in artificial intelligence. Thus, there is strong motivation to develop practically useful SAT solvers. However, the NP-completeness is cause for pessimism, since it seems unlikely that we will be able to scale the solutions to large practical instances. While attempts to develop practically useful SAT solvers have persisted for almost half a century, for the longest time it was a largely academic exercise with little hope of seeing practical use. Fortunately, several relatively recent research developments have enabled us to tackle instances with even millions of variables and constraints – enabling SAT solvers to be effectively deployed in practical applications. The problem is even (erroneously?) considered to be significantly tamed. This talk will explore this transition from theoretical hardness to practical success, including a description of the key ideas used in modern SAT solvers and future research directions.
About the Speaker: Sharad Malik received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, New Delhi, in 1985 and the M.S. and Ph.D. degrees in Computer Science from the University of California, Berkeley, in 1987 and 1990 respectively. Currently he is the George Van Ness Lothrop Professor of Engineering at Princeton University and the Chair of the Department of Electrical Engineering.
His research focuses on design methodology and design automation for computing systems. His research in functional timing analysis and propositional satisfiability has been widely used in industrial electronic design automation tools.
He has received the DAC Award for the most cited paper in the 50-year history of the conference (2013), the CAV Award for fundamental contributions to the development of high-performance Boolean satisfiability solvers (2009), the ICCAD Ten Year Retrospective Most Influential Paper Award (2011), the Princeton University President’s Award for Distinguished Teaching (2009), as well as several other best paper and teaching awards. |
