Speaker
Prof.
Uriel Feige
(Weizmann Institute)
Description
A 3SAT algorithm needs to correctly decide for every
3CNF formula whether it is satisfiable or not. We do not
expect a 3SAT algorithm to run in polynomial time,
because 3SAT is NP-hard. Nevertheless, a 3SAT
algorithm may run in polynomial time on a substantial
fraction of all 3SAT instances. Of particular interest to
this talk are random instances of 3CNF formulas with
very large density (clause to variable ratio). Such 3CNF
formulas are unlikely to be satisfiable. 3SAT algorithms
that terminate in polynomial time on most such instances
(and always give the correct answer) are referred to as
refutation heuristics. We shall survey some of the ideas
used in the design of refutation heuristics.
Primary author
Prof.
Uriel Feige
(Weizmann Institute)
