►
From YouTube: 2020.02.27 - Brown Bag: Hands on Constraint Solving
Description
Brown Bag about Constraint Solving and practical applications. Edit: During the presentation, I wrongly used the term “assigning value”. Instead, I should have said “Impose an equality constraint”; On slide 27: The v_000 is redundant. We can remove it and start from v_001 instead.
A
A
Can
you
see
my
screen
or
I'm
perfect,
so
I
wanted
to
start
with
a
little
bit
of
background,
so
I
wanted
to
do
a
short
refresher
about
boolean
algebra.
So
this
is
all
we
need
for
today
it's
about
conjunction
disjunction
and
negation.
So
you
know,
and
we
algebra
you
have-
you
have
boolean
variables
or
you
can
also
call
them
literals
and
they
can
have
two
values
true
or
false.
A
So
it's
like
a
bit
century
and
then
you
can
have
operations
between
these
variables
and
the
conjunction
is
a
logical
end
where
you
say
that
X
1
and
X
2
have
to
be
true
for
the
conjunction
to
be
true
for
this
Junction.
It's
it's
basically
the
opposite.
So
the
only
only
only
if
X,
1
and
X
2
are
both
false,
then
also
the
disjunction
is
false
and
all
the
other
cases
it's
true
and
then
you
can
have
a
negation
where
you
basically
flipping
the
bits.
A
So
if
X
1
is
2,
not
X,
1
is
false
and
vice
versa,
and
this
is
basically
all
we
need
to
know
today,
at
least
to
understand
start
solving,
essentially
and
constraint.
Solvers
can
be
used
to
to
solve
a
subset
of
problems
that
can
be
classified
as
constraint,
satisfaction,
problems
and
the
constraint
satisfaction
problems.
They
usually
consist
of
three
parts,
so
we
have
a
set
of
variables.
A
You
have
domains
of
these
variables,
so
you,
for
example,
you
can
have
integer
variables
and
the
domain
would
be
integer
domain
or
you
can
say
from
0
to
210
for
simplicity.
Let's
say
that
this
is
the
domain,
and
then
you
can
have
a
set
of
constraints
that
is
basically
relations
between
these
variables.
A
So
you
can
say
that
X
1
has
to
be
greater
than
X
2,
which
would
be
constrained,
and
the
property
of
these
constraints
is
that
they
can
be
only
false
or
true,
so
these
are
can
only
be
boolean
essentially,
and
the
whole
goal
is
to
for
for
constraint
solving,
at
least
and
for
constraint.
Satisfaction
problems
is
to
find
a
model
or
an
assignment
for
variables
that
satisfies
all
the
constraints
that
are
part
of
your
CSP.
A
So
CSP
is
basically
the
short
term
for
constraint,
satisfaction
problem
and
then
we
come
to
boolean
satisfiability,
so
boolean
satisfiability
has
been
applied
on
Hardware
verification,
so
this
was
basically
the
reason
why,
by
constraint,
solving
came
about
in
the
first
place,
so
back
in
the
70s.
They
were
basically
design
already
designing
their
their
circuit
boards
and
software,
and
they
needed
to
verify
whether
what
the
design
and
software
was
actually
correct.
A
We
have
negation
gates
and
we
have
again
an
end
gate
that
combines
these.
These
input
variables
to
produce
some
output
signal
and
this
equation
that
you
can
see
below
is
basically
the
same.
It's
representing
the
logic
that
are
the
semantics
of
the
the
circuit
that
you
can
see
here.
So
this
is
basically
the
same
thing
and
what's
nice
is
that
you
can
take
this
equation
here?
That's
basically
representing
the
logic
or
the
semantics
of
this,
so
good.
You
can
put
it
into
constraint,
solver
and
the
constraint.
A
Solver
will
tell
you
what
is
the
assignment
through
these
variables?
X1
x2
and
what
do
I
have
to
assign
to
them
to
make
the
signal
here?
True,
that's
basically
the
idea
of
of
a
Sat
solver
and
then
most
of
the
Sat
solver.
Still
today
they
use
an
input,
form
called
conjunctive
normal
form.
So
they
expect
your
set
of
equations
that
you
have
to
be
in
a
certain
format
and
the
conjunctive
normal
form
is
basically
an
end
of
ORS.
A
The
whole
equation
basically
evaluates
to
false,
and
this
is
a
design,
desirable
property
for
constraint
solving,
because
if
you
have
a
formula
designed
it
this
way
you
fail
early.
So
you
can
detect
these
false
cases
rather
early.
So
you
don't
have
to
search
too
long
to
find
a
solution,
and
what
I
should
mention,
though,
is
that
every
formula
that
you
have
can
be
translated
into
CNF.
A
So
there
are
ways
to
you
may
remember,
from
from
computer
science
classes
that
they
were
like
these
DeMorgan
rules
that
you
could
use
to
translate
logical
formulas
into
a
different
representation
that
you
could
apply
and
you
cannot.
You
can
use
them
to
translate
your
formula
into
C
and
F
2,
but
this
translation
is
not
always
easy.
So
it's
because
you
you're
basically
blowing
up
your
input,
input
formula.
So
in
the
worst
case,
this
could
lead
to
an
exponential
blow-up.
A
A
And
if
you
want
to
translate
this
and
you
see
an
F,
what
we
have
to
do
is
we
have
to
take
this
negation
and
put
it
as
if
we
move
it
inside
the
the
clauses
that
we
have
here
and
then
we
flip
the
the
operator
from
a
logical
end
to
logical
or
so
this
is
an
one
of
you,
the
Morgan.
Would
we
apply
to
trying
to
do
this
translation
and
then
we
have
our
formula
here
in
CNF.
A
What
is
just
an
example
and
the
and
then
booing
satisfiability?
They
use
a
different
kind
of
terminology
that
the
computer
scientist
would
use.
So
instead
of
variables,
they
use
the
term
literals
and
the
literal
basically
means
the
variable
or
the
negated
variable.
So
for
us,
the
negation
is
basically
an
operation,
but
from
the
perspective
of
constraint,
solving
guys
the
negation
belongs
to
the
for
the
variable
kind
of
so
it's
one
datura,
and
then
we
have
clauses
which
are
basically
the
conjunct.
A
A
So
once
we
have
know
our
formula
in
translated
into
CNF
and
we
can
pass
it
on
to
a
Sat
solver
in
this
case,
the
question
is:
how
does
this
observe
actually
determines
whether
there
is
a
model
for
this
particular
constraint
that
we
passed
on
when
I
say
model
I
mean
what
is
the
assignment
to
the
variables
to
make
the
whole
constraint
true
and
and
basically
all
the
constraint
solvers
on
most
of
the
constraint
solvers.
They
are
using
depth-first
search
for
that
and
the
first
thing
they
are
doing
is
they
are
selecting
a
variable.
A
In
many
cases,
they
use
some
heuristics
to
pick
a
variable
that
they
can
prance
on.
So
let's
say
that
the
constraint,
so
it
picks
a
variable
in
this
case
X
1,
and
sets
X
once
to
x1
to
true
and
then
the
constraint
solver
selects
the
second
variable
setting
x2
to
true
and
basically,
if
he
tries
to
solve
this
equation
with
this
input,
variables,
constraint,
solver
and
in
this
case
it's
not
possible.
So
if
you're
setting
both
variables
to
true
this
would
would
be
false.
You
cannot
solve
the
equation.
A
It
wouldn't
be
sad,
so
it's
unset
and
what
the
constraints
I
was
doing
then
is
tracking
back.
So
it's
by
going
back
one
level
up
and
then
selecting
a
different
value
for
X
2
and
now
we
have
X
1
is
2
and
X
2
is
false,
which
is
satisfiable.
So
in
this
case
we
found
the
model,
which
is
an
assignment
to
the
variables
X
1
and
X
2,
making
the
whole
constraint
set
of
constraints.
A
True-
and
this
is
basically
what
constraints
all
of
us
are
doing
internally,
but
there's
a
problem
with
that,
so
it
wouldn't
scale
for
so.
If
you're
running
this
on
on
a
constraint
set
with
100,000
million
variables,
you
have
a
search
tree,
that's
2
to
the
power
of
numbers
of
variables
that
you,
you
were
trying
to
search
a
solution
for
so
it
wouldn't
work
for
large
instances
and
therefore-
and
the
idea
was
like
a
couple
of
researchers-
it's
Davis
put
min
document
dot
length
and
they
they
all
put
their
names
into
the
algorithms
they
developed.
A
They
always
look
at
at
complete
losses
so
because
in
CNF
one
of
the
nice
properties
is
that
all
of
these
clauses
they
are
connected
with
the
conjunction
meaning
that
only
one
of
these
clauses
have
to
be
false
for
the
whole
set
instance
to
be
to
be
false
and
they
exploit
this
property
of
CNF
and
they
invented
in
the
algorithm
to
two
mechanisms.
One
is
called
unit
propagation
and
the
other
one
is
called
Hulett
or
elimination
and
for
unit
propagation.
A
What
they're
looking
at
is
once
they've
already
walked
down
the
search
field
bit,
so
they
already
fixed
certain
values
for
subset
of
variables.
There
are
some
clauses
where
you
only
have
one
variable:
that's
still
free,
so
you
can
still
pick
a
value
either
true
or
false,
and
what
it,
what
they
do
trying
to
determine
is
based
on
the
decisions
they
already
made
in
the
past.
What
has
to
what
the
value
has
to
be
for
this
particular
variable?
A
So,
let's
imagine
you
have
you
have
a
class
with
2
variables,
X
1
and
X
2,
and
you
already
selected
false
for
X
1,
so
the
value
for
X
2
has
to
be
true
in
order
for
the
whole
Clause
to
be
true-
and
this
is
like
an
approach
that
they're
using
to
make
the
search
more
efficient
so
that
they
don't
have
to
actually
search
any
more
than
it
can
basically
implicate
or
based
on
logical
implication.
They
can
derive
values
for
other
variables
and
then
there's
this
other
mechanism
called
pure
little
elimination.
A
This
is
actually
very,
very
nice
because,
when
you
they're
looking
for
clauses
where
they
only
have
where
there's
a
variable,
that
only
appears
once
so.
It
means
that
this
variable
is
not
involved
in
any
other
constraint,
so
they're,
just
picking
true
for
this
variable
to
make
the
whole
Clause
true
and
then
eliminating
the
clause
from
set
of
equations,
which
already
makes
the
search
tree
much
much
smaller
from
the
beginning
onwards,
and
then
there's
another
mechanism
called
a
conflict
driven
class
learning.
This
is
a
mechanism
that
allows
you
to
learn
from
mistakes.
A
I
will
just
show
you
an
example
in
a
second,
so
this
here's
an
example
of
of
the
DPL,
a
search
search
approach.
So
let's
assume
that
on
the
right
side,
this
is
our
set
of
constraints
or
set
instance
that
we
are
trying
to
solve,
and
here
we
are
just
randomly
selecting
one
single
class,
starting
with
that
one
where
we
have
x7
and
x8,
and
we
just
say
that
X
7
so
we're
starting
to
search
just
selecting
faults
as
an
initial
value
for
X
7.
So
because
we
selected
false
for
x7.
A
A
Here
we
fixed
x7,
so
we
cannot
select
the
value
for
X
7
anymore,
but
we
can
freely
choose
between
values,
which
was
values
for
X
9
and
X
10,
so
we
selected
through
for
X
9
and
if
we
select
into
fights
9
X
10
has
to
be
true
for
this
clause
to
be
true
and
then
we're
moving
to
the
next
class
where
you're
selecting
X
1,
it
would
be
false
and
then
X
2
has
to
be
true,
and
for
that
one
we
already
fixed
values
for
X
1.
Where
we
said
X
1
is
false.
A
We
would
come
up
with
different
values
for
X
6,
so
it's
6
can
be
either
false
can
be
both
false
and
true
at
the
same
time,
which
is
not
possible
for
for
that
server.
So,
in
this
particular
case
we
basically
observe
the
conflict,
so
we
are
tracking
back
and
we
are
selecting
different
values
for
the
variables
starting
with
with
x1
equals
to
true,
and
we
continue
doing
that
until
we
we
end
up
with
with
assignments
that
make
make
our
sub
instance
satisfiable
or
true,
and
this
is
basically
how
GPL
world
works.
A
So,
unlike
depth-first
search,
it
is
always
looking
at
the
relations
of
all
the
variables
that
we
have
and
looks,
and
within
which
constraints
is
this
variable
involved
and
based
on
that
it
makes
it
makes
decision
and
tries
to
add
and
to
infer
values
based
on
decisions
that
have
to
be
made
from
the
past
and
what's
the
benefit,
the
benefit
is
that
we
are
trimming
our
search
space.
So
we
don't.
A
Whenever
there
is
a
conflict
it
it
tries
to
to
backtrack
through
the
reason
of
this
conflict,
so
it
tries
to
identify
what
was
the
reason
and
the
constraint
solving.
They
also
call
this
the
kernel.
What
does
the
the
minimal
set
of
variables
that
that
caused
the
conflict
to
happen?
And
the
idea
is
that
when
you
have,
when
you
have
like
this
implication,
a
reason
or
conflict
follows
a
father
as
a
reason
or
is
due
to
reason
you
can
compute
the
contrapositive.
A
So
you
can
basically
flip
this
and
saying
that
if
the
conflict
doesn't
appear,
then
it
means
that
the
reason
is
also
not
there.
Then
you
just
add
this
reason.
This
negated
reason
as
a
set
of
constraint
to
your
to
your
side
instance,
and
this
basically
means
that
the
reason
that
the
Kostis
conflict
can
never
ever
happen
and
in
the
future
and
and
but
what
does
it
do?
A
It
basically
means
that
you,
instead
of
backtracking,
you're
Europe,
jumping
back
so
you
you
don't
go
back
to
two
states
that
that
are
that
are
causing
issues
or
can
cause
conflicts.
So
you
just
forward
jump
over
them
and
then
you
you,
basically
you
can
think
of
it
as
learning
from
mistakes
more
or
less.
So,
whenever
there
is
a
mistake
that
you
observe
you
are
you're
trying
to
avoid
this
mistake
in
the
future
and
that's
what
conflict
ruined
because
learning
is
about
and
yeah.
This
was
all
about.
Sat
solving.
Are
there?
C
Just
gonna
say
when
you
say
like
learning
from
your
mistakes:
it's
also
if
you
back
just
backtrack.
One
slide
in
that
example,
where
you
were
learning
from
your
mistakes.
You're
also
skipping
a
few
other
potential
mistakes.
Because
of
the
reason
that
you
just
learned
is
that
correct
sorry
then
slide
14
I
think
it's
the
one
that
I
was
talking
about
yeah.
A
C
A
So
you
don't
have
to
when
you're.
Looking
at
the
depth-first
search
example,
you
you
basically,
you
don't
really
learn
from
learn
anything
you
just
basically
exploring
the
whole
search
space
exhaustively
and-
and
here
you,
you
add,
orestes
kernel,
this
small
smallest
set
of
of
variables
that
are
leading
to
a
certain
conflict
that
you're
adding
iterative
ly
while
you're
going
through
your
search
space.
So.
C
C
A
E
A
E
D
G
B
A
You
there
are
certain
techniques
that
you
could
use,
so
I
can
imagine
it
for
security.
It
would
be
nice
to
get
a
set
of
solutions.
So
imagine
an
application
and
security
where
you
would
like
to
get
malicious
input
strings,
for
example,
and
then
you
would
like
to
get
a
set
of
let's
say:
100
attack
text
rings
that
could
could
exploit
the
given
vulnerability.
A
So
what
you
could
do
is
you
could
always
exclude
a
given
solution
explicitly
so
once
you
have
a
set
solution
and
a
model,
you
can
just
add
the
model
to
your
set
of
initial
constraints
and
saying
I.
Don't
want
to
have
this
model
again,
just
give
me
another
one,
but
there
also
as
some
tea
servers
that
are
giving
you
the
possibility
to
ask
for
another
solution.
So
you
can
ask
for
another
model,
so
we
can,
for
example
in
oh,
that's
that
set
three
you
can
ask
there
is
a
command
called
cat
model.
A
C
A
For
if
you
want
to
find
the
best
solution,
then
this
would
be
more
like
an
optimization
problem
and
and
for
force
for
constraint.
Solving
it's
more
like
shadow
answered,
yes
or
no,
and
if
you're
going
into
optimization
problems,
then
you
would
rather
use
maybe
a
search
based
approach
to
try
string
to
optimize
a
given
or
towards
a
given
target.
But
you
could
you
could
also
use
the
approach
that
you
just
mentioned
just
like
generate
thousand
models
and
pick
the
one
that
suits
you
best.
That
would
be
also
a
valid
approach,
but
yeah
I.
D
C
A
A
C
A
C
A
So
the
for
SMT
solvers
you
can,
you
can
solve
constraints
iteratively
for
such
solvers
I,
most
probably
there
also
some
that
supported
so
I'm,
actually
not
quite
sure
about
that,
but
for
SMT,
solvers,
I'm
sure
that
you
can
maintain
the
state
and
memory.
So
you
can,
you
can
add
an
ish
and
they
should
set
of
constraints,
and
you
can
always
work
backwards,
so
it
can
attract
backtrack
through
previous
states.
So
we
have
some
sort
of
a
stack
of
all
the
solutions
of
all
the
constraints
that
you've
added
and
you
can.
A
A
So
that
was
the
we
just
own
the
animations,
so
just
jump
to
this.
It
starts
right
away.
Oh
yeah!
This
is
not
just
slide
about
as
Angie
solving
so
SMT
solving
is
an
extension
of
sat
solving,
so
SMT
stands
for
satisfiability
model.
Theory
theories,
and
the
nice
thing
about,
as
in
key,
is
we're
not
limited
to
the
boolean
to
boolean
variables
anymore,
so
we
can
use,
they
call
them
theories
which
allow
you
to
solve
constraints
of
a
real
integer
integers
areas
and
the
the
I
think
in
the
recent
years.
A
They've
added
the
theory
of
strings
which
was
kind
of
hot
and
security,
at
least,
and
the
I
always
compare,
sat
and
SMT
solving.
It's
like
comparing
assembly
to
a
high-level
programming,
language
and
assembly.
You,
you
only
have
a
very
simple
set
of
primitives
that
you
have
to
know
and
an
SMT.
You
have
more
high-level
operations
that
you
can
that
you
can
use.
So
you
have
more
powerful
functions
that
you
have
at
your
disposal,
so
it's
also
easier
to
use
and
more
accessible
and,
of
course,
for
Asante.
A
You
also
have
your
own
version
of
flavor
of
DPLA,
so
you
may
come
across
DP
ll
T,
so
they
put
the
T
in
brackets.
It's
the
same
thing
like
DPL
facade.
The
only
difference
is
that
you
can
plug
in
theories.
So
what
they
want
to
emphasize
is
that
they
support
a
number
of
theories
that
you
can
use
which
also
translate
to
Sat.
A
Ultimately,
but
you
don't
see
it
so
you
use
integer
constraints
on
a
very
high
level,
and
these
are
taken
care
of
by
the
SMT
solver
translates
to
two
such
constraint
and
then
solve
by
at
core.
That's
still
part
of
of
this
SMT
solving
approach.
So
it's
for
me.
It's
like
a
framework,
that's
built
around
a
Sat
solver
and
then
the
second
part
is
so.
A
This
was
like
a
background
or
an
introduction
about
sadness
and
she's
solving
and
now,
in
the
second
part,
I
I
just
wanted
to
show
you
how
you
can
translate
problems
into
into
certain
SMT
and
what
the
differences
are
when
you're
translating
your
your
problem
into
these
different
domains
and
usually
when
you
train,
when
you
translate
a
problem,
you
you
start
off
the
problem.
We
try
to
figure
out.
How
can
I
can
I
translate
this
into
into
a
set
or
SMT
problem?
A
A
That's
basically
the
set
of
constraints
that
we
have
and
one
challenges
that
we
have
to
address
for
such
solving,
especially,
is
how
can
we
solve
this
puzzle
if
we
only
have
boolean
variables,
so
we
don't
have
numeric
variables
and
to
be
able
to
do
that.
We
have
to
add
a
third
dimension
to
our
Spokeo
puzzles,
so
for
every
cell.
In
our
in
our
Sudoku
puzzle,
we
be
adding
basically
nine
boolean
variables.
Every
single
boolean
variable
stands
for
a
number
that
we
are
signing
to
the
field.
A
So,
to
give
an
example,
here
we
have
v0u,
which
is
the
first
field
and
in
the
first
row,
and
we
have
nine
fields
and
if
v0
is
u1,
which
is
one
boolean
variable.
If
it's
true,
it
means
that
the
very
one
is
assigned
to
variable
v,
0
0.
If
V
0
is
u2,
it's
like
another
wooden
variable
that
we
have
if
we
assigned
true
to
that,
it
means
that
the
value
2
is
assigned
to
field
V,
0
0.
A
So
this
is
the
way
how
you
can
model
this
problem
in
terms
of
boolean
logic,
which
the
drawback
of
this
is
that
you
have
to
add
nine
variables
for
every
single
field
of
your
Sudoku
puzzle.
So
you
can
imagine
that
we
have
like
81
fields
and
that's
like
81
x
times,
9
variable
variables
that
you
have
to
maintain
and
to
add
to
your
to
your
problem,
constraint
and
then
the
second
part
is
we.
We
have
an
initial
setting,
so
the
initial
setup
is
the
value
or
the
values
that
are
already
present
in
our
Sudoku
puzzle.
A
So
we
have
to
reflect
this
somehow.
So
what
we
could
do
here
is
we
could
say
that
we
said
V
0
zu
9,
which
is
our
dummy
variable
for
the
for
assigning
9
to
field
V,
0
0.
To
true
we
said
we
do
to
fight
for
justice
field.
We
said
this
to
to
V
0
0
8
would
be
that
field
here
which
had
this
to
true
and
so
on.
So
this
would
be
the
initial
setup
that
we
have
for
our
supercool
puzzle.
A
Then
we
have
a
set
of
constraints
that
that
we
have
to
have
to
be
satisfied
for
for
Sudoku,
and
we
have
row
constraints
saying
that
the
in
every
row
you
can
only
use
a
unique
value
for
every
field
between
1
and
9.
The
same
is
true
for
columns
and
also
for
these
upgrades,
and
we
only
can
use
a
unique
value
and
then
there's
a
slide
catch
which
is
only
relevant
for
when
you
for
start
solving.
A
We
have
to
make
sure
that,
because
every
single
field
in
our
Sudoku
puzzle
gets
9
dummy
variables,
we
have
to
make
sure
that
we
don't
set
two
of
them
to
true.
Only
one
of
them
can
be
true
at
the
same
time.
So
this
is
something
that
that
you
have
to
make
sure,
and
especially
for
such
solving,
and
to
give
you
an
example
how
complex
these
constraints
I
can
get
is.
A
This
is
basically
the
courtesies
to
constraint
that
we
are
using
to
make
sure
that
we
don't
have
a
double
assignment
so
that
we
don't
have
to
dummy
variables
for
one
field
that
I
set
to
true
it
same
time
so
to
model
this,
we
use
for
every
dummy
variable
that
we
have
for
for
this
field.
We
use
a
disjunction
saying
that
one
of
them
should
be
should
be
true,
and
then
for
every
pair
that
we
have
for
every
pair
of
variables.
A
A
We
are
adding
for
one
field
just
to
make
sure
that
we
don't
have
a
double
assignment
and
I
will
show
you
like
how
we
how
this
is
encoded
in
a
second,
but
just
to
show
you
how
you
can
encode
this
and
to
what
the
input
format
is
today.
That's
mostly
used
by
pioneer
by
Sat
solvers,
and
this
input
format
is
called
D
max
and
it's
basically
text-based
input
format
that
you
can
use
to
to
generate
your
constraint
and
then
pass
it
on
to
the
constraint
solver
and
what
you
have
is
you
have?
A
First,
you
have
can
specify
what
the
format
of
your
constraint
is.
In
this
case
it's
conjunctive
normal
form.
Then
we
say
that
we
have
three
variables
and
just
so.
This
is
the
example,
so
we
have
three
variables:
b1,
b5
and
d4,
and
we
have
one
single
class.
So
this
is
the
clauses
we
are
trying
to
solve
and
then
0
is
used
as
a
delimiter
I.
Don't
know
why,
but
it's
a
and
then
for
translating
your
clause.
A
You
basically
use
just
indices,
just
numbers
that
are
representing
your
variables,
so
we
use
one
for
we
V
1,
5,
45
and
4.
For
me
before
and
negation
is
basically
it's
a
that
you're
using,
and
this
also
shows
you
one
of
the
the
other
problems
that
you
have
and
using
such
solving
or
when
using
T
Max
and
essentially
is
that
you
cannot
use
labeled
variables.
You
have
to
enumerate
all
your
variables
and
then
then
keep
track
of
the
mapping
somehow,
which
makes
things
a
bit
more
complicated
for
police
as
compared
to
some
G.
E
A
A
A
Can
you
see
the
determinant
there's
a
big
enough
for
okay,
so
for
for
the
for
this
demonstration
I'm
using
many
sat,
which
is
a
very
small
Sat
service
that
is
using
DPL
air
and
also
constraint,
driven
conflict,
driven
class
learning
and
our
input,
so
Doku
puzzle
is
basically
provided
as
a
CSV
file,
so
this
would
be
the
Sudoku
puzzle
will
be
trying
to
solve.
You
can
see
the
rows
here.
These
are
the
different
roles
that
we
have,
and
this
here
basically
is
the
column.
A
So
the
C
would
be
this
second
value
in
the
first
row
and
so
on.
So
this
is
our
problem
instance
and
now
we're
trying
to
solve
this
with
the
first
I
have
to
generate
my
constraints
for
that
I've
written
a
small
script
that
that
takes
this
CSV
file
and
generates
a
constraint
and
d-max
format.
So
it's
basically
generating
the
constraint
and
the
format,
and
now
we
can
see
a
file
called
input
CNF,
that's
the
demarks
input
file
and
just
to
give
you
an
idea
how
this
content
looks
like.
A
This
is
very
cryptic,
so
it's
hard
to
actually
understand
what
what's
going
on,
it's
just
a
bunch
of
numbers
that
that
you
can
see,
but
it's
it's
basically
encoding
the
problem,
as
we
saw
in
previous
slides,
it's
basically
using
exactly
the
same
approach
to
encode
the
problem
and
then
I
can
use
mini-set,
oh,
but
I
should
also
mention
here.
Is
that,
as
I
mentioned,
we
have
to
map
our
variables,
so
we
have
to
have
a
very
a
very
bad
maps.
A
The
values
that
we
have
like,
for
example,
V,
0,
Z
1,
is
mapped
to
a
natural
number
like,
which
is
fun.
Easy
oco-2
is
mapped
to
to
these
zero.
Six
three
is
not
to
another
value:
P
155
is
mapped
to
one
131
and
so
on.
So
this
is
just
to
keep
track
of
the
numbers
of
variables
of
the
names
of
the
variables
and
the
number
that
we
are
signing
to
them.
A
So,
to
solve
the
constraint,
we
can
just
involve
many
results
with
the
our
input
file,
which
is
endemics
format,
and
then
we
generate
some
output,
so
many
start
soft
our
constraints
or
return
rather
quickly,
and
when
we
looking
at
at
the
outputs
that
that
the
mini-sub
generated
it's
also,
it's
also
looking
quite
cryptic.
So
we
would
have
to
translate
this
back
somehow
into
into
a
Sudoku
setup.
So
this
is
like
the
model
that
mini
start
produced
and,
and
the
model
tells
you
all
the
values
for
all
the
fields
and
your
Sudoku
puzzle.
A
A
Just
filtering
out
the
first
few
variables
here,
so
this
is
all
about
the
the
first
three
variables
that
we
have,
so
this
here
would
be
would
be,
would
be
V,
0
0.
This
here
would
be
easier.
One
this
year
would
be
easier
to
and
regarding
the
values
this
year,
because
we
enumerated
all
the
all
the
cells
essentially
now
a
Sudoku
puzzle,
so
every
cell
that
we
haven't
I
was
a
local
puzzle,
got
assigned
a
number.
This
means
that
this
here
is
actually
the
field.
A
A
If
I'm,
taking
the
the
input,
the
input
file
and
if
I'm
counting
the
lines
we
have
like
24,000
constraints,
only
for
a
Sudoku
puzzle
with
a
size
of
9
times
9
over
9
times,
9
grid.
So
it's
quite
a
lot
of
constraints
that
you
have
to
add
in
order
to
solve
a
relatively
easy
or
simple,
simple
problem,
so
that
that
was
all
about,
sat
solving
and
how
to
solve
Sudoku
with
start
solving
and
that
we
can
move
on
to
to
SLG
solving.
A
Basically,
we
took
boolean
variables
to
mimic
a
value
assignment
and
for
Asante
we
simply
can
take
labeled
variables
and
we
can
assign
values
to
them.
So
we
can
make
use
of
the
theory
of
numbers
here,
and
we
can
just
say
that
this
0
0
is
scientific
9,
v,
0
2
is
assigned
the
value.
5
is
already
satisfied,
the
value,
8
and
so
on.
A
So
this
is
already
simpler
because
we
don't
have
to
add
this
third
dimension
to
our
problem
space
and
to
give
you
also
an
example
or
comparison
to
the
single
assignment
problem
that
we
saw
earlier
to
solve
this.
We
can
just
use
a
constraint
saying
that
easier
0
should
be
a
value
between
1
and
9.
So
it's
much
simpler
because
we
can
use
the
theory
of
numbers
and
2
to
pass
the
constraint
or
to
formulate
2
constraint
so
that
it
can
be
understood
by
an
SMT
solver.
A
We
can
use
SMT
lip
just
a
standard
standardized
input
format.
So
it's
supported
by
all
the
major
constraint
solvers
like
z3,
CVC
4,
and
the
nice
thing
is
when
you're
using
SMT
lip
or
when
you,
when
you're
formulating.
You
know
constraint
in
accordance
to
the
SMT
lib
format.
You
can
just
switch
the
constraints
over
here,
so
you
can
use
CBC
for
you.
Can
you
see
three
so
you're
flexible?
You
because
you
don't
use
the
native
the
native
language
of
the
constraint,
solver
and
yeah,
so
you
can.
A
If
you
were
interested,
you
can
find
the
specification
of
SMT
lip
2.6
here
on
this
link,
and
another
advantage
of
a
scintilla
is
that
it
does
not
require
the
input
formula
to
be
in
CNF,
so
you
are
much
more
flexible
and
the
way
you
formulate
you
the
constraints.
It
is
more
expressive
because
you
you're
not
just
limited
to
two
conjunctive
normal
form.
You
can
express
your
constraint
in
much
more
flexible
way
and
another
nice
nice
feature
of
SMT.
A
Is
it's
flexible
because
you
can
add
new
theories,
so
you
can
add,
or
it's
new
capabilities
to
constraint.
Solver
can
leverage
the
infrastructure.
That's
already
there
like
the
sidecar
and
all
of
the
translation
features
that
are
already
implemented,
and
you
can
just
focus
on
implementing
a
new
theory.
For
example,
the
string
theory
which
has
been
has
been
added
a
couple
of
years
ago
to
SN
2,
Z,
3
and
also
CDC
for
and
yes
until
it
forward,
it's
much
more
I
would
say
comparable
to
a
high-level
programming
language.
A
So
here
you
have
solver
configuration,
so
you
can
set
certain
Flags
configuration
flex.
You
can
you
have
variable
declarations
and
variable
types,
so
you
can
be
using
declare
fun
for
that.
But
it's
not
this
gates,
not
it's
not
a
function.
It's
basically
a
boolean
variable
that
you
are
declaring,
and
then
you
have
conjunct.
So
you
have
a
set
of
constraints,
but
they
don't
have
to
be
in
CNF.
A
So
and
then
usually
you
when
you've,
you
know-
and
you
have
formulated
your
constraint,
you
can
ask
the
server
to
check
satisfiability
and
give
you
the
the
model
to
assignments
to
the
variable
to
make
the
constraint
satisfiable-
and
here
we
are
I-
will
use
another
demo.
I
will
use
c3
as
an
example.
So
again
we
have
our
our
input
input
formula
which
is
in
CSV
file,
and
then
we
have
our
generation
T
script
that
generates.
Given
the
the
input
CSV
file
generates
SMT
constraint.
It
can
be
soft
by
constraint.
Swallow
then
we
as
an
output.
A
We
get
our
input
s
or
problem,
basically
as
an
SMT
constraint
and
when
you're
looking
at
the
constraint
is
much
more
easier
to
read.
So
you
basically
we
have
for
every
fields.
In
our
Sudoku
puzzle
we
have
a
variable
which
is
of
type
int.
Then
we
have
some
constraints.
This
is
the
constraint
that
basically
says
that
that
variable
should
have
a
distinct
value.
So
each
of
these
variables-
and
that
are
in
the
first
of
all-
should
have
a
distinct
value.
A
And
then
we
have
the
other
constraints
that
basically
limit
the
scope
between
values
that
are
values
between
0
and
0
and
9,
and
when
I'm
solving
this
we've
said
three
I'm
getting
the
answered.
Satisfiable
and
as
III
will
just
give
me
the
assignments
to
for
each
and
every
variable
that
we
have
in
our
constraint,
so
v-0
7
should
be
inside
5
3,
6
5
should
can
assign
3
and
so
on.
So
it's
basically,
you
don't
have
to
decrypt
the
result.
It
can
be
directly.
F
A
So
this
is
basically
here
so
here,
I'm
assigning
the
initial
initial
values
for
problem
set-
and
this
here
in
this
part,
is
just
to
make
sure
that
we
don't
use
one
value
twice.
This
is
a
nice
feature
of
SMT.
This
is
a
high
level
of
function.
That's
already
part
of
SMT,
where
you
can
have
a
collection
of
variables,
and
you
say
that
each
of
them
should
have
a
distinct
value.
A
F
A
A
It's
that's
that's
true,
I
said,
as
said
assigning,
but
it's
actually
the
wrong
term.
I
should
say
this.
There's
a
constraint
that
this
user
constraint,
which
has
to
be
true,
saying
that
v01
should
be
equals
to
three.
So
this
condition
here
should
be
true
by
the
sort
assigning
a
value.
That's
that's
a
good
point.
Yeah.
That's.
B
D
A
Here
it's
back
to
Phillip
Phillips
comments.
This
here
is
basically
redundant,
so
we
could
eliminate
V
zero
zero
zero
here.
So
we
could
just
start
from
these
zeros
u1.
Essentially
we
don't
need
this
value.
I
just
used
it
here
to
as
a
sort
of
placeholder
for
this
field.
If
this
might
make
sense,
so
it's
essentially
redundant.
We
could
leave
it
out,
but
here-
and
you
were
referring
I-
think
to
this
slide
right
here.
A
It's
basically,
we
only
have.
We
only
have
few
zero
zero,
so
we
don't
have
to
add
these
variables
at
all
just
dummy
variables.
So
this
is
it's
one
thing
that
we
do
because
as
I'm
please
higher
higher
level
and
can
deal
with
integers,
we
don't
have
to
add
this
third
dimension,
so
we
avoid
these
dummy
variables.
A
A
Okay,
so
oh
yeah,
then
I
wanted
to
shortly
talk
about
language
bindings.
So
if
you
want
to
use
a
constraint
solver,
then
you
will
find
a
lot
of
language
bindings,
that
for
various
kinds
of
languages,
so
usually
Python,
Java,
C
C++,
when
you're
using
CBC
for
and
z3.
You
usually
also
have
these
language
bindings
and
they
have
a
very
nice
API
to
manage
constraints
and
also
to
communicate
with
the
constraint
solver
and
but
one
of
the
the
biggest
advantages
I.
A
Think
of
using
the
language
binding
is
that
they
maintain
the
state
of
the
constraints
of
the
in
memory.
So
you
can
iterate
the
iteratively
kind
of
self
constraints,
which
is
much
nicer
as
compared
to
passing
on
an
SMT
like
constraint
to
the
constraints
over
that
will
give
you
an
all-or-nothing
result:
they're
doing
it
iteratively
you
can
all
backtrack.
A
As
this
is
the
example
from
the
slides,
where
we
basically
have
a
couple
of
variables
to
be
that
we're
creating,
so
we
say
that
we
have
an
integer
variable
here
and
we
adding
a
constraint
which
saying
it
should
be
smaller
than
100
and
a
couple
of
other
constraints.
So
whenever
I'm
invoking
this,
it
will
give
me
the
model,
so
it
directly
communicates
with
the
constraint,
solver
and
I
print
prints
out
the
model,
but
it
made
the
main
advantage
of
using
language.
Binding
is,
as
I
said
earlier,
that
you
can
can
do
soft
constraints
iteratively.
A
Okay,
then
the
third
or
fourth
pass
part
of
this
brown
bag
is
about
practical
applications
for
constraint.
Solving.
How
are
they
used
today
and
I
think
that
the
two
major
applications
are
model
checking
and
symbolic
execution,
so
model
checking?
This
is
basically
going
back
to
the
example
that
I
showed
earlier,
where
you
have
a
circuit
that
you
would
like
to.
A
So
it's
like
an
exhaustively
checking
whether
your
model
adheres
to
the
specification
and
the
second
part,
which
is
I,
think
more
relevant
in
our
context
as
a
body
execution
for
program
analysis
and
there
you
can,
you
can
think
of
it
as
a
combination
of
static
analysis
and
constraint
solving,
and
the
idea
is
that
you,
you
have
a
program
and
you
treat
certain
variables
of
your
program
as
symbolic
variables
and
symbolic
variables
means
that
they
are
free,
so
the
symbolic
execution
engine
can
freely
assign
values
to
these
symbolic
variables.
And
then
you
go
through
your
program.
A
You
collect
the
path
conditions
and
you
use
a
constraint
solver
to
solve
the
path
conditions
for
you.
So
whenever
you
do
encounter
a
branching
point,
you
query
the
constraints
of
a
please
give
me
some
some
model
for
the
variables
and
then
the
constraints
of
return
and
then
based
on
whatever
the
constraint.
Solver
tells
you
you
knows:
what
are
the
conditions
to
walk
down
this
path
or
what
conditions
to
walk
down
the
other
path?
And
it's
it's
been
used
to
detect
bugs
and
arrows
and
also
to
generate
test
cases
in
programs
and.
A
Is
one
problem
with
symbolic
execution
and
when
you're,
using
it
an
exhaustive,
exhaustive
Lamanna,
so
when
you're
walking
through
your
program
and
try
to
exhaustively
search
through
all
the
broken
parts
that
you
have
instead,
you,
you
might
run
into
the
so-called
path
explosion
problem.
So
you
just
have
too
many
states
that
that
you
have
to
explore,
and
another
more
subtle
issue
is
that
the
constraint
service
is
still,
although
when
using
necessity
for
a
solver
which
is
rather
powerful,
they
are
still
pretty
limited.
A
So
when
you
have
string
operations,
when
you
just
look
at
string
operations
that
you
have
in
modern
programming
languages,
there
are
many
operations
that
are
rather
complicated
or
complex
when
you
want
to
solve
them,
think
about
regular
expression,
matching,
for
example,
and
when
you're
using
them
in
combination
with
other
constraints.
This
is
still
some
something
where
constraint:
solvers
are
not
really
good
at
I.
Think
is,
if
you
have
constraints
that
there
are
going
between
different
domains.
A
Let's
suppose
you
have
a
regular
expression
constraint
and
this
regular
expression
constraint
is
connected
to
an
integer
constraints
that
is
bounding
the
string
length
or
saying
that
the
string
should
be
longer
than
X,
and
if
you
are
like
crossing
these
boundaries,
then
constraint.
Solvers
are
not
still
not
very,
not
very
efficient.
If
you
have
too
many
constraints
that
are
crossing
these
boundaries,
but
in
by
and
large
you
can,
you
can
use
them
when
you,
when
you
focus,
focus
your
attention
on
a
certain
portion
of
a
program
you
can.
A
You
can
really
use
them
in
practice,
so
they
do
really
perform.
Well,
if
you
use
some
domain
knowledge
to
just
say
that
I
want
to
focus
my
attention
on
a
certain
certain
portion
of
my
program
and
to
just
for
illustration.
I
want
to
use
clear
so
clear,
symbolic
execution
engine,
that's
used
for
LLVM
bit
code
and
it's
used
using
constraint
solving
to
decide
which
path
to
take
in
whenever
it
comes
across
a
path
condition.
It
will
invoke
the
constraint,
solver
and
determine
if
under
which
conditions
can
I
take
this
or
that
path.
A
A
D
A
Hopefully,
it's
basically
basically
used
to
to
figure
out
if
there
are
certain
arrow
states
in
your
program,
if
it
can't
find
errors,
for
example,
buffer
overflows,
and
it
will
just
check
all
the
execution
paths-
I
mean
you
can
of
course
configure
it
and
tweak
it
that
it
performs
differently,
but
in
the
default
setting
basically
goes
through
your
whole.
Your
whole
program-
and
this
is
the
program
that
I
would
like
to
use
for
this
demonstration.
A
So
it's
it's
a
small
C
program
where
you
have
an
input
buffer
and
and
and
we
are
using
an
unsafe
function-
mem
copy
here
we
are
copying
from
one
buffer
to
the
other
and
we
are
using
two
symbolic
variables.
So
you
have
to
tell
you
what
are
the
symbolic
variables
in
advance
when
I
say
symbolic
variables,
I
basically
mean
that
these
are
the
variables
that
Cree
has
control
over.
A
A
So
this
would
be
the
bc
file
that
you
can
see
here
and
then
we
running
CLE
on
this
on
this
bc
file,
and
now
it's
basically
walking
through
the
program
and
trying
to
find
error
states
and
it
was
able
to
detect
the
buffer
overflow
vulnerability
that
we
have
in
the
program,
because,
when
you're
looking
at
the
code,
you
can
see
that
the
attacker
has
control
over
the
number
of
bytes
that
should
be
copied.
So
he
can
basically
he
can
inject
whatever
he
likes
to
into
the
input
buffer.
A
So
there's
a
nice
tool
called
K
test
you
can
use
in
order
to
to
figure
out
what
were
the
conditions
under
which
this
error
was
was
produced,
and
you
can
see
that
1
0
2
was
basically
I,
think
one
that
caused
the
issue.
So
we
can
printed
out
and
then
you
can,
when
you're
going
through
this
for
this
file,
you
can
see
the
values
that
have
been
assigned
to
data,
so
this
was
the
assignment
to
data.
A
This
is
the
the
value
that
was
assigned
to
to
this
to
to
the
size
the
number
of
bytes
that
should
be
coming.
So
this
is
the
value
for
the
side
science
precise,
which
is
the
number
of
bytes
to
be
copied.
So
you
can
basically
take
take
these
values
here
and
can
reproduce
the
error
that
was
that
was
caused
by
likely
by
walking
through
these.
So
the
different
program
program,
parse.
A
So
a
as
far
as
I
know,
per
default
Klee
doesn't
shrink
that,
so
it
will
going
to
give
you
whatever
it
was
able
to
detect
in
order
to
for
for
causing
the
issue
to
happen,
and
it
will
generate
the
test
cases,
but
I'm
not
sure
there
might
be
most.
Probably
there
is
an
option
for
P
because
it
has
like
it
went
really
tons
of
options
that
you
can
configure
it
in
a
way
you
like
that
was
probably
there's
an
option
there
that
supports
that,
but
I'm
not
quite
sure
about
that.
A
So
I
have
to
check
but
and
another
interesting
files.
You
can
see
you.
This
is
the
number
the
queries
it's
like
all
queries,
as
in
Jesus,
is
the
file
that
contains
all
the
queries
that
have
been
sent
over
to
the
constraint.
Solvers
and
it's
quite
large,
so
contains
a
lot
of
a
lot
of
constraints
that
they
cheered
even
for
such
a
small
example.
They
were
actually
a
lot
of
a
lot
of
paths
that
that
were
encountered
by
CLE
because
it
works.
It
works
basically
down
also
into
a
library.
A
Is
that
basically
goes
into
library,
functions
and
checks.
Also
the
paths
inside
these
dis
library
cards,
so
this
is
basically
the
reason
why
it's
hard
to
apply
some
boring
execution
for
large
applications.
It's
basically
impossible
because
you
just
have
too
many
too
many
paths
in
your
in
your
program
to
do
that.
A
But
there
are
ways
to
to
circumvent
or
to
mitigate
these
issues
at
least-
and
this
is
touching
on
another
project
session-
that
James
will
most
probably
give
in
the
upcoming
weeks,
which
is
about,
can
colic
execution
and
they.
This
is
an
attempt
to
make
symbolic
execution,
scalable
and
and
apply
applicable
to
large
applications
by
combining
it
with
concrete
executions.
A
So
you
basically
of
concrete
inputs,
you
don't
you
don't
have
to
declare
all
your
variable
symbolic
you,
basically
every
leveraging
information
that
you
may
get
from
test
cases
or
expert
knowledge
that
may
be
provided
about
certain
variables
and
the
second
part
here.
This
is
what
I've
been
using
in
the
past.
It's
called
slicing
and
chopping,
and
the
idea-
or
if
it's
another
strategy
to
mitigate
the
path,
explosion,
problem
and
issue,
if
you
have
some
knowledge
about
the
broken
parts
that
you're
interested
in
in
advance.
A
So
that's
saying
security:
this
would
be
sources
and
things
you
can
just
extract
the
program,
that's
connecting
sources
and
syncs
with
one
another.
So
you
do
some
reachability
analysis
and
then
you
focus
do
symbolic
execution
efforts
on
these
on
these
portions.
Only
so
you
don't
execute
the
whole
program.
You
only
execute
or
symbolical
execute
a
part
of
the
program
that
is
important
to
you.
A
At
least
this
is
just
an
overview
of
the
differences
between
a
set
and
an
SMT
I
just
wanted
to
provide
a
table,
to
recap
the
differences
and
if
you're
interested,
you
will
find
more
details,
and
there
are
some
nice
talks
about
constraints
on
your
aleene's
here.
There
is
the
rice
for
fun,
where
you
can
play
with
the
three
online,
so
you
don't
have
to
install
it
on
your
machine.
A
You
can
just
play
with
some
constraints
and
then
there's
a
paper
about
TPL
and
see
how
it's
working
internally
and
yeah,
basically
both
of
papers
about
TPP
and
the
all
the
examples
from
today
you
can
find
on
my
github
profile.
So
all
the
scripts
and
everything
that
I've
used-
you
can
find
it
there
and-
and
it
was
basically
basically
it
sorry
I-
think
I
stretched
over
stretch
a
little
bit.
So
it's
six
minutes
over,
but
and
are
there
some
do?
A
D
Thank
you
so
much
for
this.
We
really
appreciate
it.
Yeah
there's
a
lot
of
fun.
It
seems
like
it's
interesting
to
think
about
its
approach
to
solving
finding
a
model,
as
opposed
to
you
know,
say
how
you
go
about
it
with
a
neural
network
where
some
of
the
other
ml
approaches,
which
are
a
little
bit
softer,
and
you
have
the
answer
already
you're,
just
trying
to
find
the
appropriate
model
to
get
to
that
answer.
Given
data,
so
are
there
any
approaches
to
speeding
any
of
this
up
to
with
like
GPUs?
A
A
Mm-Hmm
I'm,
I
can't
really
speak
about
about
using
like
GPUs
or,
if
they're,
most
probably
there
I'm
pretty
sure
that
there
is
some
work
about
that
too.
A
tool
to
apply
constraint.
Solving
on
that
I
know
that
there's
some
work
about
distributing
constraints.
So
the
idea
is
that
you,
when
you
have
a
constraint
network
to
partition
it
and
then
to
use
use
clusters
to
solve
the
constraint
I
know,
there's
some
work
in
this
area,
but
I
don't
know
how
well
this
works
in
practice.
A
I
just
know
that
there's
some
papers
that
try
to
do
that
and
it
seems
to
be
reasonable
if
you
figure
out
a
way
how
you
can
partition
your
constraints,
I
mean
it's
it's
of
course
it's
easy.
If
you
have
a
constraint
and
CNF,
then
it's
rather
simple
to
partition
your
constraint.
You
can
just
split
it
and
distribute
it
among
different
instances
or
on
your
cluster.
A
You
can
find
a
good
partitioning
scheme
and
I
I
know
that
there's
some
also
some
work
to
identify
the
clusters
of
variables,
so
the
relations
of
variables
and
to
figure
out
sub
constraint,
network
sub
constraint
networks
where
most
of
the
variables
are
involved
in
and
to
sort
of
use
that
to
as
a
strategy
to
identify
what
would
be
the
first
variable
to
branch
on,
but
yeah,
that's
regarding
GPU
and
mattresses.
I
can
every
kind
of
really
give
a
good
answer
to
that.
So.
D
E
D
F
Was
gonna
say,
there's
one
more
thought
on
so,
let's
say
we're
using
Klee
or
innocent
II
solver
to
explore
all
paths
of
a
program.
Buzzing
has
the
same
goal:
right
yeah.
You
have
to
generated
input,
you
have
that
up
front,
you
generate
it
and
you
know,
send
it
down
the
path,
and
so
it
really
depends
on
what
your
goals
are
and
kind
of
what
the
application
is.
F
It's
SMT
solving
is
a
bit
more
logical
instead
of
random,
but
there
are
ways
to
do
guided
fuzzing
so
that
it
has
a
feedback
mechanism
so
that
it
knows
if
it's
going
into
further
areas,
and
so
a
lot
of
modern
fuzzers
use
something
like
that
as
well
and
they're
extremely
fast.
But
there's
one
guy
follow
on
twitter.
He
or
his
Twitter
handle
is
Galasso
labs
or
Komodo
labs.
Something
like
that,
but
a
lot
of
his
researches
and
writing
custom
hypervisors
for
fuzzing
and
he's
doing
like
hundreds
of
millions
of
test
cases
per
second.