To check satisfiability of a formula, we would have to construct a proof tree where the formula occurs on the left hand side only, and no formula is on the right hand side. The tool is only made for validity, and therefore we start with the negated formula on the right hand side. The next node will be the one you would like to really start with.
Hence, this is just for technical reasons. But you can also say that a formula phi is satisfied by any counterexample shown that its negation is not valid.
