The Computational Complexity of Satisfiability
Download
Report
Transcript The Computational Complexity of Satisfiability
The Computational
Complexity of Satisfiability
Lance Fortnow
NEC Laboratories America
Boolean Formula
u v w u w x v w x
u v w x: variables take on TRUE or FALSE
u NOT u
u OR v
u AND v
vu
v u
Assignment
u v w u w x v w x
u TRUE
v FALSE
w FALSE
x TRUE
Satisfying Assignment
u v w u w x v w x
u TRUE
v FALSE
w TRUE
x TRUE
Satisfiability
u v w u w x v w x
A formula is satisfiable if it has a
satisfying assignment.
SAT is the set of formula with satisfying
assignments.
SAT is in the class NP, the set of problems
with easily verifiable witnesses.
NP-Completeness of SAT
In 1971, Cook and Levin showed
that SAT is NP-complete.
NP-Completeness of SAT
SAT
A
In 1971, Cook and Levin showed
that SAT is NP-complete.
Every set A in NP reduces to SAT.
NP-Completeness of SAT
f
SAT
A
In 1971, Cook and Levin showed
that SAT is NP-complete.
Every set A in NP reduces to SAT.
NP-Completeness of SAT
f
SAT
A
True even for SAT in 3-CNF form.
u v w u w x v w x
NP-Complete Problems
SAT has same complexity as
Map Coloring
Traveling Salesman
Job Scheduling
Integer Programming
Clique
…
Questions about SAT
How much time and memory do we need
to determine satisfiability?
Can one prove that a formula is
not satisfiable?
Are two SAT questions better
than one?
Is SAT the same as every other NPcomplete set?
Can we solve SAT quickly on other models
of computation?
How Much Time and
Memory Do We Need to
Determine Satisfiability?
Solving SAT
2n
T
I
M
E
n
log n
SPACE
n
Solving SAT
2n
T
I
M
E
n
log n
SPACE
n
Search all of the
assignments.
Best known for
general formulas.
Solving SAT
2n
Can solve 2-CNF
formula quickly.
u w u v u v
T
I
M
E
n
2-CNF
log n
SPACE
n
Solving SAT
2n
T
I
M
E
n
log n
SPACE
n
Solving SAT
Schöning (1999)
3-CNF satisfiability
solvable in
time (4/3)n
2n
1.33n
3-CNF
T
I
M
E
n
log n
SPACE
n
Schöning’s Algorithm
Pick an assignment a at random.
Repeat 3n times:
If a is satisfying then HALT
Pick an unsatisfied clause.
Pick a random variable x in that clause.
Flip the truth value of a(x).
Pick a new a and try again.
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
P = NP
n
log n
SPACE
n
Is SAT computable
in polynomialtime?
Equivalent to
P = NP question.
Clay Math Institute
Millennium Prize
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
P = NP
?
n
log n
SPACE
n
Can we solve SAT
in linear time?
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
Does SAT have
a linear-time
algorithm?
nc
P = NP
n
log n
SPACE
n
Unknown.
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
Does SAT have
a linear-time
algorithm?
nc
?
P = NP
n
log n
SPACE
n
Unknown.
Does SAT have a
log-space
algorithm?
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
Does SAT have
a linear-time
algorithm?
nc
P = NP
Does SAT have a
log-space
algorithm?
n
log n
SPACE
n
Unknown.
Unknown.
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
n
P = NP
?
log n
SPACE
n
Does SAT have
an algorithm that
uses linear time
and logarithmic
space?
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
Does SAT have
an algorithm that
uses linear time
and logarithmic
space?
nc
n
P = NP
X
log n
SPACE
n
No! [Fortnow ’99]
Idea of Separation
Assume SAT can be solved in linear
time and logarithmic space.
Show certain alternating automata
can be simulated in log-space.
Nepomnjaščiĭ (1970) shows such
machines can simulate superlogarithmic space.
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
P = NP
n1.618
n
log n
SPACE
n
Improved by
Lipton-Viglas and
Fortnow-van
Melkebeek.
Impossible in
time na and
polylogarithmic
space for any a
less than the
Golden Ratio.
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
P = NP
n1.618
n
log n
SPACE
Fortnow and van
Melkebeek ’00
n
More General TimeSpace Tradeoffs
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
P = NP
n1.618
n
log n
SPACE
Fortnow and van
Melkebeek ’00
n
More General TimeSpace Tradeoffs
Current State of
Knowledge for
Worst Case
Solving SAT
2n
1.33n
T
I
M
E
3-CNF
nc
P = NP
n1.618
n
log n
SPACE
Fortnow and van
Melkebeek ’00
n
More General TimeSpace Tradeoffs
Current State of
Knowledge for
Worst Case
Other Work on
Random Instances
Can One Prove That a
Formula is not Satisfiable?
SAT as Proof Verification
u v u v
SAT as Proof Verification
u v u v
is satisfiable
u = True; v = True
SAT as Proof Verification
u u v u v
SAT as Proof Verification
u u v u v
is satisfiable
SAT as Proof Verification
u u v u v
is satisfiable
Cannot produce
satisfying assignment
Verifying Unsatisfiability
u u v u v
Verifying Unsatisfiability
u u v u v
u = true; v = true
Verifying Unsatisfiability
u v u v
Verifying Unsatisfiability
u v u v
u = true; v = false
Verifying Unsatisfiability
Not possible unless NP = co-NP
Interactive Proof System
Interactive Proof System
HTTHHHTH
Interactive Proof System
HTTHHHTH
010101000110
Interactive Proof System
HTTHHHTH
010101000110
THTHHTHHTTH
001111001010
Interactive Proof System
HTTHHHTH
010101000110
THTHHTHHTTH
001111001010
THTTHHHHTTHHH
100100011110101
Interactive Proof System
Developed in 1985 by Babai
and Goldwasser-Micali-Rackoff
HTTHHHTH
010101000110
THTHHTHHTTH
001111001010
THTTHHHHTTHHH
100100011110101
Interactive Proof System
Lund-Fortnow-Karloff-Nisan 1990: There is an
interactive proof system for showing a formula
not satisfiable.
HTTHHHTH
010101000110
THTHHTHHTTH
001111001010
THTTHHHHTTHHH
100100011110101
Interactive Proof for co-SAT
u u v u v
u (1 u) v (1 u) (1 v)
For any u in {0,1} and v in {0,1} value is zero.
Interactive Proof for co-SAT
u (1 u) v (1 u) (1 v)
Interactive Proof for co-SAT
1
1
u (1 u) v (1 u) (1 v)
u 0 v 0
Value is zero.
Interactive Proof for co-SAT
1
u (1 u) v (1 u) (1 v )
v 0
u 3u 2u
3
2
Interactive Proof for co-SAT
1
u (1 u) v (1 u) (1 v )
v 0
1
u
u 0
3
3u 2u 0
2
Interactive Proof for co-SAT
1
u (1 u) v (1 u) (1 v )
v 0
u 3u 2u
3
2
Picks u at random, say u = 17.
u 3u 2u 4080
3
2
Interactive Proof for co-SAT
1
u (1 u) v (1 u) (1 v )
v 0
u = 17
4080
Interactive Proof for co-SAT
1
17 (1 17) v (1 17) (1 v)
v 0
u = 17
4080
Interactive Proof for co-SAT
17 (1 17) v (1 17) (1 v)
17v 17v 4080
2
Interactive Proof for co-SAT
17 (1 17) v (1 17) (1 v)
1
17v
2
17v 4080 4080
v 0
u = 17
4080
Interactive Proof for co-SAT
17 (1 17) v (1 17) (1 v)
17v 17v 4080
2
Pick random v, say v=6.
17v 17v 4080 3570
2
u = 17
v=6
3570
Interactive Proof for co-SAT
u (1 u) v (1 u) (1 v)
Plug in 17 for u and 6 for v.
Evaluates to 3570.
A PERFECT MATCH!
u = 17
v=6
3570
Interactive Proof for co-SAT
If formula was satisfiable
then any evil prover would
fail with high probability.
Uses fact that polynomials
are low-degree.
Two low-degree
polynomials cannot agree
on many places.
Extensions
Shamir 1990
Interactive Proof System for
every PSPACE language.
GMW/BCC 1990
SAT has interactive proof
that does not reveal any
information about the
satisfying assignment.
Probabilistically Checkable
Proof Systems
Probabilistically Checkable
Proof Systems
Queries bits
of the proof
Defined by Fortnow-Rompel-Sipser 1988
Probabilistically Checkable
Proof Systems
Queries bits
of the proof
Babai-Fortnow-Lund 1990
PCP = NEXP
Probabilistically Checkable
Proof Systems
Queries bits
of the proof
Babai-Fortnow-Levin-Szegedy 1991
Roughly linear-size proof of SAT verifiable
with small number of queries.
Probabilistically Checkable
Proof Systems
Queries bits
of the proof
ALMSS 1991
Proofs of SAT using constant queries and
logarithmic number of random coins.
Probabilistically Checkable
Proof Systems
Queries bits
of the proof
ALMSS 1991
Many applications for showing hardness of
approximation for optimization problems.
Hard to Approximate
Clique Size
Traveling Salesman
Max-Sat
Shortest Vector in Lattice
Graph Coloring
Independent Set
…
Are Two SAT Questions
Better Than One?
Questions to SAT
Oracle willing to honestly answer
a limited number of SAT questions.
Does the number of queries matter?
Focus on what happens if two
queries to SAT can be simulated by a
single SAT query.
Are Two Queries Better
Than One?
Series of results by
Kadin 1988
Wagner 1988
Chang-Kadin 1990
Amir-Beigel-Gasarch 1990
Beigel-Chang-Ogihara 1993
Buhrman-Fortnow 1998
Fortnow-Pavan-Sengupta 2002
If One Query as Powerful as
Two Queries …
Any polynomial number of
adaptive SAT queries, can
be simulated by a single
SAT query.
Polynomial-Time hierarchy collapses
to Symmetric Polynomial-Time.
Alternation
Alternation
Model invented
by CKS 1981.
Unbounded
Alternation
= PSPACE
Alternation
Model invented
by CKS 1981.
Constant
Alternation
=
Polynomial
Hierarchy
Symmetric P
Symmetric P
Defined by Russell
and Sundaram 1996
If One Query as Powerful as
Two Queries …
If One Query as Powerful as
Two Queries …
Hard-Easy Strings
If one query as powerful as two then
for every unsatisfiable , either
There is a nondeterministic proof that
is not satisfiable, or
One can use as advice to solve
satisfiability for all formulas of the
same length.
Proofs use applications of this fact.
Is SAT the Same as Every
Other NP-Complete Set?
NP-Completeness of SAT
*
*
f
A
SAT
Isomorphisms of SAT
*
*
f
SAT
A
A set A is isomorphic to SAT if A
reduces to SAT via a 1-1, onto,
easily computable and invertible
reduction.
Are all NP-complete sets
the same as SAT?
*
*
f
SAT
A
Berman and Hartmanis 1978
All of the known NP-complete sets are
isomorphic.
Are all NP-complete sets
the same as SAT?
*
*
f
SAT
A
Berman and Hartmanis 1978
Conjecture: All of the NP-complete sets
are isomorphic.
Are all NP-complete sets
the same as SAT?
*
*
f
SAT
A
If conjecture is true…
All NP-complete sets, like SAT, must
have an exponential number of strings
at every length.
What if SAT reduces to a
small set?
Mahaney’s Theorem (1978)
Ogihara and Watanabe (1991)
For many-one reduction then P=NP.
For reductions that ask a constant
number of queries still P=NP.
Karp-Lipton(1980)/Sengupta(2001)
For arbitrary reductions, polynomial
hierarchy collapses to Symmetric-P.
Are all NP-complete sets
the same as SAT?
*
*
f
SAT
A
Still Open
Look at relativized worlds
Universes that show us limitations of
most proof techniques.
Are all NP-complete sets
the same as SAT?
*
*
f
SAT
A
Fenner-Fortnow-Kurtz 1992
A relativized world where the
isomorphism conjecture holds.
Can We Solve SAT Quickly
on Other Models of
Computation?
Solving SAT on Other
Models of Computation
RANDOM
DNA
QUANTUM
Can we solve SAT Quickly
with Random Coins?
Would imply collapse of the
polynomial-time hierarchy.
Reasonable assumptions imply
randomness computation not
any stronger than deterministic
computation.
IW ’97: If EXP does not have
subexponential-size circuits then we
can derandomize.
Can we solve SAT Quickly
with DNA Computing?
Adleman has solved TSP on 20
cities with DNA manipulation.
Problem: Exponential Growth
Exponential Growth
20 Cities
Exponential Growth
75 Cities
Can we solve SAT Quickly
with DNA Computing?
Adleman has solved TSP on 20
cities with DNA manipulation.
Problem: Exponential Growth
Adleman
The less pleasing part is that we
learned enough about our
methods to conclude that they
would not allow us to
outperform electronic
computers.
Can we solve SAT Quickly
on a Quantum Computer?
Basic element is qubit that
is in a superposition of zero
and one.
N qubits can be entangled to
form 2N quantum states.
States can have negative
amplitudes that can cancel
each other out.
Transformations are limited
to a unitary manner.
Can we solve SAT Quickly
on a Quantum Computer?
Shor 1994
Factoring can be solved
quickly on a quantum
computer.
Grover 1996
Search a database of size N
using N1/2 queries.
Yields quadratic improvement
for general satisfiability.
Best possible in a black-box
model.
Can we solve SAT Quickly
on a Quantum Computer?
Fortnow-Rogers
Relativized world where
quantum computing is no
easier than classical, yet
PNP and the polynomial
hierarchy does not collapse.
Physical Difficulties
Maintain Entanglement
Handle Errors
High Precision
Other Research
Lower Bounds for proving nonsatisfiabilility in weak logical models.
Circuit complexity approaches to
lower bounds for satisfiability.
Solving SAT on “Typical” instances.
Many other structural questions
about satisfiability.
Conclusions
The satisfiability question captures
nondeterministic computation and
much of the interest in
computational complexity.
We have made much progress on
these fronts but many questions
remain.
Prove PNP!