...
Proof
...
Complexity
...
and
...
Complexity
...
of
...
SAT
...
Solvers
...
This
...
talk
...
discusses
...
the
...
performance
...
of
...
a
...
SAT
...
solvers
...
from
...
the
...
perpective
...
of
...
computational
...
complexity
...
and
...
proof
...
complexity.
...
The
...
first
...
half
...
of
...
the
...
talk
...
discussed
...
the
...
"bad
...
news"
...
from
...
the
...
point
...
of
...
view
...
of
...
the
...
hardness
...
of
...
nondeterministic
...
polynomial
...
time
...
(NP)
...
and
...
complexity
...
aspects
...
of
...
the
...
hardness
...
of
...
proof
...
search.
...
The
...
second
...
half
...
addresses
...
the
...
"good
...
news"
...
that
...
DPLL
...
solvers
...
with
...
clause
...
learning
...
are
...
very
...
efficient
...
for
...
many
...
practical
...
problems.
...
We
...
discuss
...
the
...
performance
...
of
...
the
...
SatDiego
...
solver
...
on
...
the
...
pigeonhole
...
principles.
...
We
...
discuss
...
characterizations
...
of
...
DPLL
...
with
...
clause
...
learning
...
in
...
terms
...
of
...
proof
...
systems.
...
We
...
discuss
...
the
...
effectiveness
...
of
...
restarts.
...
Sam Buss, University of California, San Diego, USA
Sam Buss is a professor of mathematics and computer science at the University of California, San Diego. He earned his Ph.D. in Mathematics in
1985 from Princeton, was the Mathematical Sciences Research Institute for 1985-1986, and the Department of Mathematics at UC Berkeley during
1986-1988. He has been at UC San Diego since 1988. His research concerns mathematical logic and theoretical computer science, especially proof
theory, bounded arithmetic, computational complexity and proof complexity. He is the author of a book on bounded arithmetic and a book on computer
graphics, and the editor of the handbook in proof theory. His current research also includes work on a SAT solver, SatDiego.
| Attachments | ||
|---|---|---|
|