A logical formula is unsatisfiable if and only if for the formula to be true, at least one of its variables must be both true and false.
I discovered SAT today, and wanted to try my hands at solving it. I arrived at the above statement as a general principle for any attempt I want to make at solving SAT. Is the principle true?
Assuming it has at least one variable (I say this, because $\bot$ is unsatisfiable and, if you are working with clauses, the clause $\{ \}$ is unsatisfiable, but neither has at least one variable), then yes, that's correct, because the right hand side basically says:
'If formula $F$ is true, then some variable $P$ is both true and false'
... which is to say: the truth of the formula $F$ leads to a contradiction,
...which means that $F$ cannot be true, which means that $F$ is unsatisfiable
So: your right hand side implies the left hand side.
And of course the left hand side implies the right hand side, since if $F$ is unsatisfiable, then $F$ is a contradiction, and so $F$ implies everything, including that one of its variables (again, assuming it has a variable) is both true and false.