Acapulco, Mexico, 2003.
We introduce the notion of a "backdoor" variable of a SAT problem
instance to explain some of the remarkable efficiency of current
SAT solvers on very large instances. The bottom line is that many
real-world instances reduce to a tractable form once a small group
of variables (the "backdoor") is set correctly. Heuristics and
restarts in current solvers are effective at identifying such variables.
Talk. Note: the latest
results on this line of research were presented
at AAAS-05 (Washington, DC).