| |
|
|
Electronic Systems Design Seminar
|
|
|
|
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.
