3
$\begingroup$

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?

Examples:

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.

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ Indeed, coNP-complete, since a counterexample is a truth assignment satisfying $F$ but not $A$. $\endgroup$
    – Yuval Filmus
    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
    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
    Jul 11, 2017 at 7:28

Your Answer

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

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