When: Monday, May 05, 12:00 p.m.

Where: 4623Wean Hall

Himanshu Jain

Speaking Skills Talk

Abstract:
The Boolean satisfiability (SAT) problem decides whether a given Boolean formula has a satisfying assignment. The SAT problem is of central importance in various areas of computer science. There has been significant (empirical) improvements in the capacity of SAT solvers over the past decade. Current SAT solvers can check the satisfiability of structured formulas containing thousands to millions of variables in reasonable time.

I will review the basic algorithm and the key ideas of search space pruning, learning, and non-chronological backtracking that are used in state-of-the-art SAT solvers. I will then discuss some of our recent work on non-clausal SAT solvers and present encouraging experimental results.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

<< Back