Title: How to refute random nonsatisfiable formulas 

Abstract: 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.