I am aware that satisfiability is NP complete and unsatisfiability is co-NP complete. But somehow I feel that labeling satisfiability as NP-complete and unsatisfiability as co-NP complete is papering over the fact that unsatisfiability (or equivalently validity) is inherently a harder problem than satisfiability. Suppose I have a NDTM. Then given a potential model I can surely check it in polynomial time. However to check unsatisfiability I would need to check all possible assignments, surely this makes the problem EXPTIME?
However to check unsatisfiability I would need to check all possible assignments, surely this makes the problem EXPTIME?
Well, $EXPTIME$ but not necessarily $EXPTIME$-complete.
Congratulations, you've found the (possible) difference between $NP$ and $Co-NP$.
The first thing to realize is that there's a duality here. Satisfiability requires only a single example to prove a YES, but (as far as we know) needs to search a possibly exponential space for a NO. Unsat is the exact dual of this: you need to search a possibly exponential set to prove a YES, but a single counter-example will prove a NO. So neither is a harder problem, it's just that one is easy for YES, and the other is easy for NO.
The second thing to realize is that every NP-complete problem has a dual like this, and that's exactly why we study $Co-NP$ complete problems. For Hamiltonian Path, one path proves it, and a full search is needed to disprove. The converse is true to for NOHAMPATH, it's complement problem. Every NP-problem has a dual by switching the "yes" and "no" cases.
Nobody knows if $NP = EXPTIME$, though it's pretty unlikely. But it seems like just having to do an exponential search isn't enough to characterize all exponential algorithms.
No, it just means that there's no obvious algorithm for a nondeterministic Turing machine to check unsatisfiability in polynomial time, which is part of the reason why we don't know if NP and co-NP are the same thing.
For deterministic machines, unsatisfiability can't be harder than satisfiability since, if you could solve either one, you could solve the other by negating the answer. Negating the answer is non-trivial for nondeterministic machines.