# Is there and efficient procedure to test whether a clause is implied by a given CNF formula?

I have a CNF formula $$F$$ and a clause $$c$$ defined on the same set of variables. I would like to know if $$c$$ is implied by $$F$$ i.e. if $$F \vDash c$$. To achieve this I could just test if the formula $$F\wedge \bar{c}$$ is unsatisfiable where $$\bar{c}=\bigwedge_{x \in c}\neg x$$. But this requires to solve instances of the boolean satisfiability problem which is known to be NP-complete.

Is there and efficient (poly-time) procedure to test whether a clause is implied by a given CNF formula?

• Your question is not research level. $F \models c$ is equivalent to testing whether $F \wedge \bar{c}$ is UNSAT thus you should actually feel that it is somewhat as hard as solving UNSAT. To prove it formally, apply it to the empty clause $\bot$. $F \models \bot$ iff $F$ is unsat. Thus, if you can solve your problem for any $c$ in PTIME, then you can decide whether $F$ is UNSAT in PTIME, a notorious coNP-complete problem ; which seems unlikely. – holf Dec 30 '18 at 7:20