Tractability of forcing-invariant statements under large cardinals It is usual to mention theorems of the kind:
Th. Assume there is a proper class of Woodin cardinals, $\mathbb{P} $ is a partial order and $G \subseteq \mathbb{P}$ is V-generic, then $V \models \phi \iff V[G] \models \phi$ 
where $\phi$ is some set theoretic statement (like "the Strong Omega Conjecture holds"), as some sort of evidence that $\phi$ is a statement less intractable than other statements like CH which are not focing-invariant.
My question is, in wich sense are these statements more tractable? What kind of "empirical evidence" gives support to the hope that they can be decided by large cardinal axioms?
 A: We have numerous statements that are invariant by set
forcing, but which are independent of ZFC and even of ZFC +
large cardinals. Thus, I dispute the premise of your question. 
Examples include:


*

*Eventual GCH. This is the assertion that the GCH holds
for all sufficiently large cardinals. This is forcing
invariant, by set forcing (see remarks below), since any
given forcing notion can affect the continuum function
only for cardinals of size less than the size of the
forcing. But it is independent of ZFC, since it is implied
by GCH and it is easy to use class forcing to produce
models with unbounded violations of GCH.

*Eventual non-GCH, or eventual some-other-GCH-pattern.
Similarly, we can arrange other GCH patterns just as easily,
and as long as the statement is only that
the pattern holds eventually, then it will again be independent
of ZFC for the same reason.

*The previous examples are also independent of ZFC+ large
cardinals, since we can control the GCH pattern while
preserving most of the standard large cardinal notions.

*Any kind of eventual statement, about a feature that can
be controlled locally by forcing. For example, assertions about the
eventual pattern of the existence
of $\kappa$-Souslin trees or $\Diamond_\kappa^*$
and so on. These can be controlled by forcing in a class
iteration to achieve unbounded patterns, but set forcing
can only affect things locally. So the statement that the
eventual pattern is such-and-such will be invariant by
set-forcing.

*Assertions that there are a proper class of
such-and-such large cardinals. These are forcing invariant,
because by the Levy-Solovay theorem, the large cardinals above the size of any
forcing will be preserved. Thus, the assertion that there
is a proper class of inaccessible cardinals, or Woodin
cardinals or supercompact cardinals, etc. are all forcing
invariant, but we cannot hope to settle these assertions
in ZFC, or even with ZFC + very strong large cardinal axioms not of this particular form.
For example, it is consistent (from a suitable hypothesis) with a supercompact
cardinal (or any other standard large cardinal notion) that there is not a proper class of inaccessible
cardinals. It is consistent with an almost huge cardinal that there is a proper class of supercomapct cardinals, and also that there is not (assuming a suitable LC hypothesis). 

*The failure of the Ground Axiom. The Ground Axiom, which I introduced with Jonas
Reitz, is the assertion that the universe is
not a set-forcing extension of any inner model. Despite
its second-order nature, it is actually first-order
expressible. GA is true in L and  forceable over
any model of ZFC by class forcing, but once it fails, then
of course it remains false in any set forcing extension.
So $\neg GA$ is upwards forcing invariant by set forcing.
And again, we get the independence here not just over ZFC,
but over ZFC + large cardinals.

*There are other similar examples concerning the
existence of  bedrock models, that is, ground models of
the universe that are not themselves forcing extensions of
any inner model.
All of these statements are forcing-invariant in the sense you mention, but none of them are settled either way by large cardinal axioms.
Set forcing vs. class forcing. It is important in
your example and all my examples above that we are speaking
of forcing invariance by set forcing, that is, when the
partial order is a set, rather than a proper class. Your
example theorem, for example, is true for set forcing,
but not for class forcing. In particular, the statement
that there is a proper class of Woodin cardinals is itself
destroyable by class forcing: one can perform the
coding-the-universe forcing that obtains $V[G]=L[x]$ for a
real $x$, and there are no Woodin cardinals in $L[x]$.
So you are only talking about forcing invariance for set
forcing to begin with. Furthermore, the assertion that
"$\varphi$ is set forcing invariant" is first-order
expressible for set forcing, but not for class forcing.
Thus, it is difficult to formalize or even express any
general theory about forcing invariance by class forcing,
although one can adopt ad hoc methods for particular
statements.
A: There are two ingredients in your question:  First, statements invariant under forcing and second, large cardinals.  The existence of certain large cardinals is a strengthening of ZFC.
Somewhat surprisingly, the known large cardinal axioms are essentially linearly ordered, i.e.,
given two such axioms, the consistency of one implies the consistency of the other.
Most set theorists believe that these large cardinal axioms are consistent.
Hence there is a natural direction to strengthen ZFC, namely by adding large cardinal axioms.
If we want to do mathematics, why not work in the strongest possible theory?  Hence we assume
that large cardinals exist (like a proper class of Woodins).
Why are forcing invariant statements less intractable than others?  Well,
simply because there is some hope that the statement can be decided in ZFC, or 
in ZFC + large cardinals, which we believe in.
Moreover, if $\phi$ is invariant under forcing, we can actually use forcing to prove or disprove $\phi$.
An example is the Baumgartner-Hajnal partition theorem, a Ramsey like statement.
In the original proof it is shown that the statement is forcing invariant and follows from
Martin's Axiom.  Since Martin's Axiom can be forced over every set-theoretic universe,
this shows that the Baumgartner-Hajnal statement is actually true in every model of set theory.
Now, of course there may be statements that are invariant under forcing, in particular
statements about the natural numbers such as the Riemann hypothesis or P=NP, that might 
not be decidable in ZFC + large cardinals.  
We currently have no method to prove independence results over ZFC other than forcing,
inner models and consistency strength (the existence of a large cardinal cannot be proved
in ZFC, because from the existence of the L.C. it follows that ZFC is consistent, but by the second incompleteness theorem this cannot be proved in ZFC (unless, of course, ZFC is inconsistent)).
If we are confronted with a statement that is forcing invariant, yet not decided by ZFC + LC, this statement is actually less tractable than others, because we currently may not have any way of proving its independence over ZFC + LC.
A: Typically, generic absoluteness is a consequence of a stronger property, that in many cases is really the goal one is after. To explain this stronger property, let me begin by reviewing two important absoluteness results.
1) The first is Mostowski's Absoluteness. Suppose $\phi$ is $\Sigma^1_1(a)$, where $a\in\omega^\omega$. This means that $\phi(x)$ for $x\in\omega^\omega$, asserts

$∃y\in\omega^\omega\forall n\in \omega R(x\upharpoonright n, y\upharpoonright n,a\upharpoonright n)$,

where $R$ is a predicate recursive in $a$. These statements are very absolute: Suppose that $M$ is a well-founded model of a decent fragment of ZF, and that $a,x\in M$. Then $\phi(x)$ holds iff $M\models \phi(x)$. 
In particular, whether or not $\phi(x)$ holds cannot be changed by forcing, or by passing to an inner or outer model. Note that $M$ could be countable. In fact, only needs to be an $\omega$-model; well-foundedness is not necessary.
This is how the result is usually stated. What is going on is the following:
Suppose that $T$ is a tree (in the descriptive set theoretic sense) and that $T\in M$. Then $T$ is ill-founded iff $M\models T$ is ill-founded. 
In particular, $T$ could be the tree associated to $\phi$. This is the tree of all $(s,t)$ such that $s,t$ are finite sequences of the same length $l$, and $\forall n\le l$ $ R(s\upharpoonright l,t\upharpoonright n,a\upharpoonright n)$. So $T$ is the tree of attempts to verify $\phi$: $\phi(x)$ holds iff (there is a $y$ such that for all $n$, $(x\upharpoonright n,y\upharpoonright n)\in T$) iff the tree $T_x$ is ill-founded. Recall that $T_x$ consists of all $t$ such that, if $l$ is the length of $t$, then $(x\upharpoonright n,t\upharpoonright n)\in T$ for all $n\le l$.
The point is that $T$ is a very simple object. As soon as $T,x$ are present, $T_x$ can be built, and the result of the construction of $T_x$ is the same whether it is performed in $V$ or in $M$. Since well-foundedness is absolute, whether or not $T_x$ is ill-founded is the same whether we check this in $M$ or in $V$. Of course, $T_x$ is ill-founded iff $\phi(x)$ holds. 
The moral is that the truth of $\Sigma^1_1$ statements is certified by trees. And I think that this is saying that in a strong sense, $\Sigma^1_1$ statements are very tractable. All we need to check their validity is a very easy to build tree and, once we have it, the tree is our certificate of truth or falsehood, this cannot be altered. 
Recall that proofs in first-order logic can be described by means of certain finite trees. If something is provable, the tree is a very robust certificate. This is a natural weakening of that idea.
Of course one could argue that, if a $\Sigma^1_1$ statement is not provable, then in fact it may be very hard to establish its truth value, so tractability is not clear. Sure. But, independently of whether or not one can prove something or other, the certificate establishing this truth value is present from the beginning. One does not need to worry that this truth value may change by changing the model one is investigating.
2) The second, and best known, absoluteness result, is Shoenfield's absoluteness. Suppose $\phi$ is $\Sigma^1_2(a)$. This means that $\phi(x)$ holds iff 

$\exists y\forall z\exists n$ $R(y\upharpoonright n,z\upharpoonright n,x\upharpoonright n,a\upharpoonright n)$,

where $R$ is recursive in $a$. Let $M$ be any transitive model of a decent fragment of ZFC, and suppose that $\omega_1\subset M$ and $a,x\in M$. Then $\phi(x)$ holds iff $M\models\phi(x)$.
This is again a very strong absoluteness statement. Again, if one manages to show the consistency of $\phi(x)$ by, for example, passing to an inner model or a forcing extension, then in fact one has proved its truth. 
Again, one could say that if $\phi$ is not provable, then it is in fact not very tractable at all. But the point is that to investigate $\phi$, one can use any tools whatsoever. One only needs to worry about its consistency, for example, and one can make use of any combinatorial statements that one could add to the universe by forcing. 
Just as in the previous case, $\Sigma^1_2$ statements can be certified by trees. The tree associated to $\phi$ is more complicated than in the previous case, and it is now a tree of $\omega\times\omega_1$. (Jech's and Kanamori's books explain carefully its construction.) Again, the tree is very absolute: As soon as we have $a$ and all the countable ordinals at our disposal, the tree can be constructed. (One comparing two models $M\subset V$, we mean all the countable ordinals of $V$, even if $M$'s version of $\omega_1$ is smaller.) 
3) Generic absoluteness of a statement $\phi$ is typically a consequence of the existence of absolutely complemented trees associated to $\phi$. In fact, all generic absoluteness results I'm aware of are established by proving that there are such trees ("conditional" generic absoluteness results, such as only for proper forcings, or only in the presence of additional axioms, are somewhat different). This is a direct generalization of the situations above.
To define the key concept, recall that if $A$ is a tree of $\omega\times X$, then the projection $p[A]$ of $A$ is the set of all $x\in\omega^\omega$ such that $\exists f\in X^\omega\forall n\in\omega\,(x\upharpoonright n,f\upharpoonright n)\in A$.
Two (proper class) trees $A$ and $B$ on $\omega\times ORD$ are absolutely complemented iff:


*

*$p[A]\cap p[B]=\emptyset$ and $p[A]\cup p[B]=\omega^\omega$.

*Item 1 holds in all generic extensions.


A statement $\phi$ admits such a pair iff, in addition,


*

*In any forcing extension, $\phi(x)$ iff $x\in p[A]$.


The idea is that this is a precise, formal, definable approximation to the intuitive statement one would actually like, namely, that there are such trees describing $\phi$ that have this ``complementary'' behavior in all outer models. First-order logic limits ourselves to considering forcing extensions.
Let me point out that $\Sigma^1_1$ and $\Sigma^1_2$ statements admit absolutely complemented pairs, so the existence of such a pair is a natural (far reaching) generalization of the two cases above. 
Once we accept large cardinals, we can show that much larger classes than $\Sigma^1_2$ admit absolutely complemented trees. For example, any projective statement does. Once again, the point is that as soon as we have the large cardinals and real parameters in our universe, we have the trees, and the trees certify in unambiguous forcing-unchangeable terms, whether the statements hold at any given real. It is in this sense that we consider these statements more tractable.
Here is a rough sketch of an example I particularly like, due to Martin-Solovay (for measurables) and Woodin (in its optimal form). For details, see my paper with Ralf Schindler, ``projective well-orderings of the reals,'' Arch. Math. Logic (2006) 45:783–793:

$V$ is closed under sharps iff $V$ is $\Sigma^1_3$-absolute. $(*)$

The right hand side means that for any $\Sigma^1_3$ statement $\phi$ (so now we have three alternations of quantifiers) and any two step forcing ${\mathbb P}∗\dot{\mathbb Q}$, for any $G$, ${\mathbb P}$-generic over $V$, any $H$, ${\mathbb Q}$-generic over $V[G]$, and for any real $x$ in $V[G]$, we have 
 $$ V[G]\models\phi(x)\Longleftrightarrow V[G][H]\models\phi(x). $$
The left hand side of $(*)$ is a weakening of "there is a proper class of measurable cardinals", which is how the statement is usually presented. 
The proof of the implication from left to right in $(*)$ goes by building a tree of attempts to find a witness to the negation of a $\Sigma^1_2$ statement. The goal is that if such a witness can be added by forcing, then in fact we can find one in the ground model. If there is a forcing adding a witness, there is a countable transitive model where this is the case. Essentially, the tree gives the construction of such a model, bit by bit, and if we have a branch, then we have such a model. 
So: If there is a witness added in a forcing extension, the tree will have there a branch. So it is illfounded. By absoluteness of well-foundedness, the tree has a branch in $V$. The sharps are used to ``stretch'' the model so that we can use Shoenfield absoluteness, and conclude that there must be a witness in $V$. 
4) Projective absoluteness, a consequence of large cardinals, is established by showing the existence of absolutely complemented trees for any projective statement. The theory of universally Baire sets originates with this concept, and the closely related notion of homogeneously Suslin trees. All of this is also connected to determinacy. Once again, to drive the point home: Generic absoluteness is not the goal. The goal is the existence of the pair of trees. Once we have them, we have a strong certificate of truth or falsehood of a statement. I do not know if one is to accept the search for such trees as a more tractable problem than the original statement whose pair of trees we are now searching for. But it certainly says that consistency of the statement, using large cardinals or any combinatorial tools whatsoever, is enough to have a proof of the statement. This seems much more hopeful and generous an approach than if only proofs in the usual sense are allowed. The existence of these trees for projective statements is what I meant in a comment by ``large cardinals settle second order arithmetic.'' Put yet another way: If you show, for example, that a projective statement is not 'decidable' (in the presence of large cardinals), meaning that it is consistent and so is its negation, then you have either actually showed that certain large cardinals are inconsistent, or you have found a way of changing the truth of arithmetic statements, and both of these options are much more significant events than the proof of whatever the projective statement you were interested in was. More likely than not, the truth value of the statement will be uncovered at some point, and you know there is no ambiguity as of what it would be, since the witnessing trees are already present in the universe.  
(In spite of its length, I am not completely happy with this answer, but I would need to get much more technical to expand on the many interesting points that your question raises. Hopefully there is some food for thought here. For nice references to some of the issues I mention here, Woodin's article in the Notices is a good place to start, and Steel's paper on the derived model theorem has much of the details.)
