...
Introduction
...
to
...
Satisfiability
...
Solving
...
with
...
Practical
...
Applications
...
This
...
talk
...
is
...
divided
...
into
...
two
...
parts
...
of
...
roughly
...
equal
...
length.
...
The
...
first
...
part
...
introduces
...
the
...
most
...
important
...
techniques
...
of
...
a
...
modern,
...
incremental
...
CDCL
...
SAT-solver.
...
The
...
second
...
part
...
discusses
...
applications
...
of
...
SAT,
...
and
...
explains
...
some
...
common
...
techniques
...
one
...
can
...
use
...
when
...
engineering
...
an
...
efficient
...
algorithm
...
with
...
a
...
SAT-solver
...
as
...
a
...
component.
...
Niklas Een, University of California, Berkeley, USA
Niklas finished his Ph.D.
...
on
...
SAT
...
based
...
formal
...
verification
...
in
...
2005,
...
and
...
has
...
continued
...
to
...
work
...
as
...
a
...
researcher,
...
first
...
at
...
Cadence
...
Berkeley
...
Labs,
...
and
...
later
...
at
...
University
...
of
...
California,
...
Berkeley.
...
He
...
is
...
mostly
...
known
...
for
...
co-authoring
...
the
...
SAT-solver
...
MiniSat,
...
but
...
his
...
interests
...
also
...
include
...
hardware
...
verification
...
and
...
logic
...
synthesis.
...
| Attachments |
|---|
...
|
...
|
...