The ZFC provability box is equivalent to a good SAT solver, up to a constant factor (and I don't see any reason to prefer one over the other). I think that the SAT solver metaphor is more familiar to most people and closer to practice, so I'd use that one unless there is some consideration pointing the other way.
Comments
Eliezer Yudkowsky
I think that many readers will have an easier time imagining 'what we can do by knowing a theorem is true, without knowing the proof' than the much more abstract case of 'knowing an NP-hard satisfiability problem was solved, without knowing the satisfaction', but you're correct that the Oracle idiom generalizes to the latter case.
Paul Christiano
I don't see why getting the satisfying assignment really matters. If your AI sometimes declines to answer, then it can cause trouble anyway. If your AI always tries "its best" to answer, then you can just ask "Is there a satisfying solution that starts with 1? With 0?" though admittedly this is less efficient.
Which example is better may depend on your audience and your possible concerns.