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?

  • 2
    $\begingroup$ 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. $\endgroup$ – holf Dec 30 '18 at 7:20

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.