When you say "naive SAT solver" do you mean one where you hard-code a boolean formula with N variables and then check every possible solution (from 0 to 2^N)? If so, does this kind of program accurately characterize the kind of work a kernel does?
No, something like the CDCL algorithm without domain specific heuristics and tweaks. I expect that is fairly representative in terms of ..say.. common data structures needed in most systems.
