A validator claims a rule's condition can never be satisfied by any request — which complexity class is that claim complete for?

## The claim is literally unsatisfiability 'This condition can never be satisfied by any request' is the statement that a boolean formula has **no** satisfying assignment. Strip the policy vocabulary and it is the classic decision problem `UNSAT`: given a formula, decide whether every assignment falsifies it. Its complement is `SAT`: decide whether some assignment satisfies it. One problem, one boundary, two names depending on which side you stand on. ## Complementing a complete problem Satisfiability is **NP-complete** — it is in NP, and every problem in NP reduces to it in polynomial time, which is the content of the Cook-Levin theorem. Now complement everything: - If `A` reduces to `B` by a polynomial-time map, the same map reduces the complement of `A` to the complement of `B`, because a many-one reduction preserves the verdict on both sides. - So if every problem in NP reduces to `SAT`, every problem in co-NP reduces to `UNSAT`. - And `UNSAT` is in co-NP by definition, since its complement `SAT` is in NP. Together those give **`UNSAT` is co-NP-complete**. The general fact is worth carrying: the complement of an NP-complete problem is co-NP-complete, never NP-complete again unless the two classes coincide. ## The tautology twin A formula is a **tautology** when every assignment satisfies it. Negate it: the assignments that satisfy the negation are exactly those that falsify the original. So `phi` is a tautology if and only if `not phi` is unsatisfiable, and negation is a linear-time transformation. Hardness travels across it in both directions, which is why tautology is the other standard co-NP-complete problem and why the two are usually named as a pair. ## Normal form decides which half is easy Both questions become trivial on the normal form that suits them, and this is the detail interviewers use to check you understand which quantifier is doing the work: | Formula shape | Is it satisfiable? | Is it a tautology? | |---|---|---| | Conjunctive normal form (an AND of clauses) | NP-complete | polynomial: every clause must contain some variable together with its negation | | Disjunctive normal form (an OR of terms) | polynomial: some term must contain no variable together with its negation | co-NP-complete | The rule behind the table: a conjunctive form makes the *falsifying* witness easy to reason about clause by clause, and a disjunctive form makes the *satisfying* witness easy to reason about term by term. Converting between the forms is what costs — the conversion can blow up exponentially, which is where the hardness hides rather than disappearing. ## What this means for the policy validator Suppose the table check is 'no request triggers two opposing rules'. Map an arbitrary formula `phi` onto a two-rule table: one rule permits when `phi` holds, one rule denies unconditionally. Then some request triggers both exactly when `phi` is satisfiable, so the table is conflict-free exactly when `phi` is unsatisfiable. That is a polynomial-time reduction **from** `UNSAT` **to** the conflict-free check, and its direction matters: 1. Reducing `A` to `B` shows `B` is at least as hard as `A` — any fast algorithm for `B` would yield a fast algorithm for `A`. 2. Here `A` is `UNSAT`, which is co-NP-complete, and `B` is the conflict-free check. 3. Therefore the conflict-free check is **co-NP-hard**. Getting this arrow backwards — concluding that `UNSAT` inherits something from the check — is the single most common error in this material. So the validator's universal claim is not merely inconvenient; it is as hard as anything in co-NP, and no clever engineering removes that while the condition language stays expressive. ## What a proof of unsatisfiability actually costs A refutation is a certificate: a derivation that a checker replays step by step, in time polynomial in the derivation's own length. That last clause is the catch. The check is fast in the size of the proof, but the proof itself need not be small — for some families of formulas, including the pigeonhole formulas, every resolution refutation is known to be superpolynomially long. So 'unsatisfiable, with a machine-checkable derivation attached' is a real and useful output format, and simultaneously not a promise of a short proof. Whether *some* proof system always gives short refutations is the NP versus co-NP question in another costume.