camGates and Hillman Centers Photo Tour
School of Computer Science, carnegie Mellon
Computer Science Department
Human-Computer Interaction Inst
Institute for Software Research
Lane Ctr for Computational Biology
Language Technologies Institute
Machine Learning Department
Robotics Institute
Entertainment Technology Center
Extended Menu Contact Info Directory About SCS SCS New Buildings Info Giving to SCS SCS Dean's Advisory Board

SCS DISTINGUISHED LECTURE SERIES
4:00 PM - Wean Hall 7500
3:45 PM Distinguished Donuts - Outside the Hall

The Gaschnig/Oakley Memorial Lecture

Sharad Malik
Professor of Electrical Engineering
Department of Electrical Engineering
Princeton University

The Quest for Efficient Boolean Satisfiability Solvers

The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this talk I will examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather I will focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, I will focus on techniques within the basic DPLL search framework, but will also briefly describe other approaches. At appropriate places, I will provide details on the Chaff SAT solver developed in our group.

Speaker Bio:

Sharad Malik received the B. Tech. degree in Electrical Engineering from the Indian Institute of Technology, New Delhi, India 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 Professor in the Department of Electrical Engineering, Princeton University. His research spans all aspects of Electronic Design Automation. His current focus areas are the synthesis and verification of digital systems and embedded computer systems. He has received the President of India's Gold Medal for academic excellence (1985), the IBM Faculty Development Award (1991), an NSF Research Initiation Award (1992), Princeton University Rheinstein Faculty Award (1994), the NSF Young Investigator Award (1994), Best Paper Awards at the IEEE International Conference on Computer Design (1992), ACM/IEEE Design Automation Conference (1996), IEEE/ACM Design Automation and Test in Europe Conference (2003); the Walter C. Johnson Prize for Teaching Excellence (1993) and the Princeton University Engineering Council Excellence in Teaching Award (1993, 1994, 1995). He serves/has served on the program committees of DAC, ICCAD and ICCD and as the General Chair for DAC 2004. He is on the editorial boards of the Journal of VLSI Signal Processing, Design Automation for Embedded Systems and IEEE Design and Test. He is a fellow of the IEEE. He is currently serving as the Associate Director of the MARCO/DARPA Gigascale Systems Research Center, a multi-university effort directed towards defining and developing system design methodology with a ten year horizon.

He has published numerous papers, book chapters and a book (Static Timing Analysis for Embedded Software) describing his research. His research in functional timing analysis and propositional satisfiability has been widely used in industrial electronic design automation tools.

<< Back