Entail is co-NP-complete under polynomial-time many-one reductions. For valid propositional formulas, semantic entailment holds exactly when the logical conjunction of the premise and the conclusion's logical negation is an unsatisfiable Boolean formula:A counterexample to semantic entailment is a Boolean valuation making true and false. Guessing one bit for each distinct Boolean variable and evaluating both propositional formulas is a polynomial-time algorithm. Thus the complement of Entail belongs to NP. Malformed descriptions, also in that complement, can be accepted after a deterministic syntax check. Hence Entail belongs to co-NP as a formal language over all strings.
For hardness, the unsatisfiable Boolean formula problem is co-NP-hard: if , then , and the permitted NP-hardness of SAT supplies a polynomial-time many-one reduction withWe may ensure is always a valid propositional formula, replacing any malformed output by a fixed contradiction. It follows that exactly when is unsatisfiable. This justifies using the unsatisfiability problem as a hardness source without an extra assumption.
Map a valid propositional formula towhere is a fixed Boolean variable. The second propositional formula is false under every Boolean valuation. Consequently it is entailed by precisely when no Boolean valuation satisfies . ThusThe output has only constant additional length and is computable in polynomial time. If the source unsatisfiability language rejects malformed strings, map them to the fixed no-instance . This completes a total polynomial-time many-one reduction and proves the claimed co-NP-completeness.
Articles by others on the same topic
There are currently no matching articles.