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.
$(\lnot a\lor b) \land (a \lor b)$
Here the atom
a can be removed, as the formula can be reduced to simply
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.)