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.


1 Answer 1


Suppose we had a TM $M$ which, given $F$ and some atomic $A$ occurring in $F$ it can efficiently (PTIME) decide whether all models of $F$ make $A$ true, i.e. whether $F \models A$.

Then we can efficiently decide the validity of any formula $G$ as follows.

Take $A$ to be any atom not in $G$. Craft $F := \lnot (G \land (\top \lor A))$, and use $M$ to decide if $F \models A$.

We then have $$ (F \models A) \iff (F \models \bot) \iff \models \lnot F \iff \models G \land (\top \lor A) \iff \models G $$

The first $\iff$ is nontrival, but easy to prove by considering the models where $A$ holds, and the others where $\lnot A$ holds, and exploiting our choice of $A$. It is left as an exercise ;-)

So, we constructed a polynomial reduction of validity to this problem. Since validity is coNP hard, we deduce this problem is also coNP hard.

  • 2
    $\begingroup$ Indeed, coNP-complete, since a counterexample is a truth assignment satisfying $F$ but not $A$. $\endgroup$ Commented Jul 10, 2017 at 15:22
  • $\begingroup$ This answers the question regarding complexity. Do you also know if this problem has a specific name in literature and if there is a better approach than just using a co-NP solver? $\endgroup$
    – Martin
    Commented Jul 11, 2017 at 7:24
  • $\begingroup$ @Martin I am not aware of any specific name. I don't think there will be a much better approach than using a validity / SAT solver. $\endgroup$
    – chi
    Commented Jul 11, 2017 at 7:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.