The Search for Satisfying Solutions
When a bug in Pentium processors was discovered that gave rise to incorrect solutions of scientific and mathematical calculations, the company was forced to take action. The result? Public outcry and the loss of $475 million worth of earnings.
It’s been almost two decades since the Pentium FDIV bug made headlines, but its discovery led to a new research thrust in computer science and engineering – one that Professor Sharad Malik, Chair of the Department of Electrical Engineering at Princeton University, knows quite well.
“It’s an instance of how real practical concerns have driven solutions to real, fundamental problems,” said Malik.
The incident brought the examination of Boolean Satisfiability or SAT, the challenge of determining if a logic formula will ever evaluate to true, to the forefront. In proving the correctness, this problem has a direct application to hardware and software and more specifically, avoiding costly bugs. SAT was already well known in computer science, but theoretical analysis deemed it to be too difficult to be applied in practice.
Malik is one of the nation’s experts on the topic, and his group has made several critical contributions to the field of SAT solvers that are now widely used in practice. On January 29, he visited Boston University to share his findings during the Department of Electrical & Computer Engineering Distinguished Lecture Series, which brings groundbreaking engineers to campus.
Currently, there is a strong motivation to discover useful SAT solvers thanks to all of the potential practical uses, such as in applications in artificial intelligence, circuit synthesis, and malware analysis.
“It’s already very widely used in hardware verification and we’re seeing an increasing use of the theory in software verification,” added Malik.
Though the SAT problem may be relatively unknown outside computer science and engineering, a very active community of researchers exists and can be found sharing their research and questions on the website, SAT Live!
Malik notes that the biggest change he’s noticed with SAT studies over the years is a revolution in how the topic is approached.
“There has been a significant shift from theoretical interest in SAT to how it can have a practical impact,” he said. What was once considered practically impossible due to its theoretical hardness is now within reach thanks to challenge-driven algorithmic and experimental research.
Malik’s talk was the first in the three-part Spring 2014 Distinguished Lecture Series. The next talk features Professor C. V. Hollot of University of Massachusetts, Amherst, who will speak on the topic, “Regulation of Cell Populations in Individuals Using Feedback-Based Drug-Dosing Protocols.” Hear him on March 5, 2014, at 4 p.m. in Room 211 of the Photonics Center, located at 8 Saint Mary’s St.
-Rachel Harrington (firstname.lastname@example.org)