Electronic Systems Design Seminar

What SAT-solvers can and cannot do

Dr. Eugene Goldberg 
Cadence Berkeley Labs


Monday, May 12, 2003, 4:00pm-5:00pm
540AB, Cory Hall, UC Berkeley


The most successful existing SAT-solvers like Chaff or BerkMin are based on the proof system called general resolution. For almost two decades it has been known that general resolution has exponential lower bounds on some classes of formulas (like pigeon-hole formulas). However, the impressive performance of the state-of-the-art solvers suggests that in most "real-life" applications we deal with formulas that have short resolution proofs.  So the next question to ask is "is there  a SAT-solver that is able to find a short proof  (or its "good" approximation) if  it exists?". In terms of complexity theory this question is formulated as "Is general resolution automatizable?". The common belief is that the answer is "no".

My talk will consist of three parts. In the first part, I will introduce a class of formulas that explains why general resolution is (most probably) non-automatizable. These formulas describe equivalence checking of Boolean circuits N1, N2 produced from a common specification S. The common specification S is just a circuit of multi-valued gates called blocks and circuits N1 and N2 are obtained from S by binary encoding of its multi-valued variables. I will show that in general resolution there is a proof of equivalence of N1 and N2 whose size is linear in the number of blocks in S.

The good news is that if the common specification S of N1 and N2 is known, then there is a deterministic algorithm whose run time is also linear in the number of blocks in S. This result suggests that it is very important to have algorithms that are more receptive to information about  high-level structure of the formula than existing SAT-solvers. In second and third parts of my talk I will describe two  proof systems that can serve as  a basis for such algorithms.  The first proof system is based on the fact that to prove that a CNF formula is unsatisfiable it is sufficient to show that this formula is unsatisfiable on a set of points called stable. The second proof system exploits the idea that to prove a formula F to be unsatisfiable one just needs to show that the set of points falsififying F (i.e. setting F to 0) is stable.



Eugene Goldberg received his M.S. degree in theoretical physics from the Belorussian State University in 1983 and his Ph.D. degree in computer science from the Institute of Engineering Cybernetics of the Belorussian Academy of Sciences in 1995.  From 1983 to 1995 he worked as a researcher in the laboratory of logic design at the Institute of Engineering Cybernetics. From 1996 to 1997 he was a visiting scholar at the University of California at Berkeley. He joined Cadence Berkeley Labs in November 1997. His main interests are development of efficient algorithms for computationally hard problems with emphasis on  CAD applications.

©2002-2018 U.C. Regents