Documentation

Complexitylib.SAT.ThreeSAT.Headline

3SAT is in NP #

This file combines the ordinary SAT witness with the regular exact-3 syntax condition. On paired inputs the resulting verifier language is the intersection of the existing SAT verifier language and ThreeSAT.PairSyntax.language, so it is in P. The generic linear-witness guess-and-verify construction then gives the headline theorem ThreeSAT.language_mem_NP.

source
def Complexity.SAT.ThreeSAT.Witness (z witness : List Bool) :
Prop

A 3SAT witness is an ordinary SAT witness whose encoded formula also has exact-3 syntax.

Equations
Instances For
    source
    theorem Complexity.SAT.ThreeSAT.witness_length_le (z witness : List Bool) (h : Witness z witness) :
    witness.length ≤ z.length + 1

    Every 3SAT witness has the same linear length bound as its SAT witness.

    source
    theorem Complexity.SAT.ThreeSAT.mem_language_iff_witness (z : List Bool) :
    z ∈ language ↔ ∃ (witness : List Bool), Witness z witness

    Exact-3 satisfiability is characterized by the combined witness relation.

    source
    theorem Complexity.SAT.ThreeSAT.pairLang_witness_eq :
    pairLang Witness = pairLang SAT.Witness ∩ PairSyntax.language

    The paired 3SAT witness language is the intersection of the SAT verifier language and the paired exact-3 syntax language.

    source
    theorem Complexity.SAT.ThreeSAT.pairLang_witness_mem_P :
    pairLang Witness ∈ P

    The combined paired verifier language is in P.

    source
    theorem Complexity.SAT.ThreeSAT.language_mem_NP :
    language ∈ NP

    3SAT ∈ NP. Exact-3 satisfiability has linearly bounded witnesses and a deterministic polynomial-time verifier.