Prof. Karem Sakallah shares 2009 CAV Award for fundamental work on SAT solvers

EECS Professor Karem Sakallah, his former graduate student Joao Marques-Silva (now at University College Dublin), and five other researchers received the 2009 Computer Aided Verification (CAV) Award this summer at the 21st International CAV Conference, which was held in Grenoble, France. The award recognizes the researchers’ series of fundamental contributions to the development of high-performance Boolean satisfiability solvers.

The seven recipients of this year’s award worked in two different teams, one at the University of Michigan and one at Princeton University, where they created powerful programs for checking whether a logic formula has a consistent solution. This is known as a “Boolean satisfiability problem,” and is named for the 19th century British logician George Boole. Their work touched off a flurry of activity that continues to this day, as teams from around the world compete to produce new satisfiability solvers, or “SAT solvers,” that can solve the most difficult problems, and to find new ways to apply these solvers to a variety of practical problems.

Sakallah and Marques-Silva’s GRASP solver, developed at the University of Michigan and first described at the 1996 International Conference on Computer-Aided Design (ICCAD), started with a classic algorithm, devised by Davis, Putnam, Logemann, and Loveland (hence known as “DPLL”) in 1962. DPLL applies backtracking search to enumerate different assignments to the variables of a formula until either a solution is found or the set of possible solutions is exhausted. Sakallah and Marques-Silva modified the DPLL algorithm to more effectively detect large classes of assignments that cannot possibly yield satisfying solutions. In doing so, they shifted the core strategy of SAT solvers from one of searching for a solution to one of pruning away the unsatisfying assignments. This change in strategy was critical to the successful application of GRASP to verification problems, where formulas typically have very few, if any, satisfying solutions (because such solutions signify errors in the system being verified.) They also changed the method of measuring SAT solver performance away from solving randomly generated problems to one of solving benchmark problems arising from real-world examples. This shift favors tuning SAT solvers to take advantage of structures and characteristics found in actual systems.

The CAV conference is the premier international event for reporting research on Computer Aided Verification, a subdiscipline of Computer Science that is concerned with ensuring that software and hardware systems operate correctly and reliably. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. The CAV award was established in 2008 by the conference’s steering committee and was given this year for the second time.