Suppose we have a propositional boolean formula F and let M be the set of all models of that formula.
I am wondering if there is an efficient way to find all atomic propositions that are implied by the formula. Informally, this means that they can only have one specific value in all models M.
Does this problem have a specific name in literature? What is the complexity?
Formula "(A)": the predicate A is implied by the formula, it can only ever have the truth value true in any model of the formula.
Formula "(A or B)": no predicate is implied by the formula, there are models where A is false, there are models where A is true, there are models where B is false, there are models where B is true.
Formula "A and (B or C)": in all models of this formula, A has to be true.