Electrical & Computer Engineering     |     Carnegie Mellon

Wednesday, March 5, 12:00-1:00 p.m. HH-1112


Hui Xu
Carnegie Mellon University

sub-SAT: A Formulation for Relaxed Satisfiability and its Application

Recent progress on solvers for Boolean SAT motivates interest in casting more and more large and complicated problems as Boolean problems. But in many cases, a legitimate criticism of these approaches is the lack of any partial solution whenever an intrinsically unsatisfiable problem is encountered. In this work we value the SAT solution style in large part because it allows us to express and solve a very large number of concurrent constraints. We present a formulation for "subset satisfiable" Boolean SAT (sub-SAT for short): we transform the CNF description of an arbitrary SAT problem into a new, relaxed SAT problem that is satisfiable just if some number k of the clauses in the formulation are ignored. Although the transformed problem is relaxed (it admits more solutions), the CNF form of the problem is larger; our construction augments the CNF with new variables and clauses representing those parts of the problem that we may allow to "opt out" of the solution. Examples from FPGA routing show how we can determine efficiently when we can satisfy "almost all" of our geometric constraints. We also use sub-SAT on randomly generated SAT problems to analyze the Phase Transition phenomenon.

Hui Xu received the B.S. and M.S. degrees in Electrical Engineering from Shanghai Jiaotong University, China, in 1997 and 2000, respectively. She is currently pursuing her Ph.D. degree in the Department of Electrical and Computer Engineering with Prof. Rob A. Rutenbar at Carnegie Mellon University, Pittsburgh, PA. Her research interests include computer aided design algorithms for physical design of ASICs and FPGAs, Boolean satisfiability method and applications.