[_delirium]

Yeah, this has led to the odd situation in AI that reducing to SAT is how you show a problem is easy--- there's a whole cottage industry of people speeding up algorithms by reducing them to SAT, and it's often seen as a promising result for your computational tractability if you can do so.

(And the biggest problems, when they arise, are usually actually in the reduction itself---it takes too damn long to write out the SAT problem. Once you've got the SAT problem written out, solving it is rarely an issue.)