Remove unneeded atoms in CNF minimalization (SAT preprocessing) This might be a very basic question.

I am interested in all atoms of a propositional formula that can be removed from a particular formula, while the derived formula has the same satisfiability characteristics.

Consider:

$(\lnot a\lor b) \land (a \lor b)$

Here the atom a can be removed, as the formula can be reduced to simply b.

Is there a name for atoms that can be removed from a formula? I.e., atoms like a that can be removed from a formula? (Informally I would call them "don't care" atoms.)

There are certain tools like lingeling and minisat2 that can simplify or preprocess a SAT problem, given a CNF formula (see another answer). 
Do this approaches reliably remove all atoms (like aabove) from the formula that can be removed? My rough guess would be that finding a minified formula is as complex as finding all the prime implicants of a formula? (Minification in my sense would be a formula with the least number of atoms.)
As Kyle Jones has mentioned, the example you provided is called (restricted) resolution. 

Beside that, pure literals can also be safely removed from a SAT problem. Unit clauses can be assigned a truth value. Check this paper:

The Puzzling Role of Simplification in Propositional Satisfiability.  Inês Lynce and João Marques-Silva.

It discusses several preprocessing techniques for SAT, and its experiments showed that applying preprocessing for SAT leads to mix results. However, this paper might not be state-of-the-art.