Occurrence list of a CNF formula to SAT is in NP if its verifier is polynomial-time

DefinitionOccurrence list of a CNF formula#✓fully proved

For a CNF formula \(\varphi = (C_1, \dots, C_m)\), the occurrence list of \(\varphi\) is the list of the variable indices of its literals, in order: the variables of the literals of \(C_1\) in order, then those of \(C_2\), and so on up to \(C_m\). Duplicates are kept, so a variable appears once for each literal in which it occurs.

def varsOf (φ : CNF) : List Nat := φ.flatMap fun C => C.map Prod.fst

Uses 2 · Used by 22

Statement usesCNF formula · CNF clause

Used byPreimage of SAT under a polynomial-time map is in NP · Variables of a formula occur in its occurrence list · The SAT verifier · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · Length of the occurrence list · The clause check on the occurrence table is the formula check · Occurrence table of a formula and a witness · The SAT verifier's answer through the occurrence table · Tokenizer run on all clauses · Rejecting run · Accepting run of the SAT tokenizer · The TM2 SAT verifier · Distinct variables of a formula · HAMPATH emitter, phase A: the clauses of a formula · Phase A of the HAMPATH emitter · Correctness and running time of the HAMPATH emitter · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction) · Positions in the list of distinct variables · Tokenize, then emit

DefinitionWitness lookup#✓fully proved

Given a list \(N = (n_1, \dots, n_k)\) of natural numbers, a list \(w = (b_1, \dots, b_m)\) of booleans and a natural number \(x\), the lookup of \(x\) in \(N\) and \(w\) is the timed computation (a returned boolean together with a natural-number cost) that scans the pairs \((n_1, b_1), (n_2, b_2), \dots\) in order, charging one tick for each pair it examines, and returns \(b_i\) for the first \(i\) with \(n_i = x\); if either list runs out first, it returns false at no further cost.

It is used with \(N\) the variables occurring in a formula and \(w\) the witness values, so the first occurrence of a variable wins.

def lookupVar : List Nat → List Bool → Nat → TimeM Nat Bool
  | [], _, _ => pure false
  | _, [], _ => pure false
  | n :: ns, b :: bs, x =>
      TimeM.tick 1 >>= fun _ =>
        if x = n then pure b else lookupVar ns bs x

Used by 10

Used byPreimage of SAT under a polynomial-time map is in NP · Clause check against a witness · Correctness of the witness clause check · Cost bound for the witness clause check · Correctness of the witness formula check · Lookup in the witness of an assignment · Cost bound for witness lookup · The SAT verifier verifies SAT · The clause check on the occurrence table is the formula check · Table lookup agrees with the verifier's variable lookup

DefinitionClause check against a witness#✓fully proved

Given a list \(N\) of natural numbers, a list \(w\) of booleans and a CNF clause \(C\), the check of \(C\) against \(N\) and \(w\) is the timed computation (a returned boolean together with a natural-number cost) that scans the literals \((x, b)\) of \(C\) in order: for each it charges one tick, then looks up \(x\) in \(N\) and \(w\), paying the cost of the lookup, and returns true if the value found equals the polarity \(b\); otherwise it moves on to the next literal. When the literals are exhausted it returns false at no further cost; in particular the empty clause fails.

def checkClause (vars : List Nat) (w : List Bool) :
    CNFClause → TimeM Nat Bool
  | [] => pure false
  | l :: ls =>
      TimeM.tick 1 >>= fun _ =>
        lookupVar vars w l.1 >>= fun v =>
          if v = l.2 then pure true else checkClause vars w ls

Uses 2 · Used by 5

Statement usesWitness lookup · CNF clause

Used byCorrectness of the witness clause check · Cost bound for the witness clause check · Formula check against a witness · Correctness of the witness formula check · Cost bound for the witness formula check

DefinitionFormula check against a witness#✓fully proved

Given a list \(N\) of natural numbers, a list \(w\) of booleans and a CNF formula \(\varphi\), the check of \(\varphi\) against \(N\) and \(w\) is the timed computation that runs the clause check against \(N\) and \(w\) on the clauses of \(\varphi\) in order, adding up their costs, and returns false as soon as one of them returns false. If every clause check returns true, in particular if \(\varphi\) has no clauses, it returns true.

def checkCNF (vars : List Nat) (w : List Bool) : CNF → TimeM Nat Bool
  | [] => pure true
  | C :: Cs =>
      checkClause vars w C >>= fun ok =>
        if ok = true then checkCNF vars w Cs else pure false

Uses 3 · Used by 10

Statement usesClause check against a witness · CNF formula · CNF clause

Used byPreimage of SAT under a polynomial-time map is in NP · Correctness of the witness formula check · Cost bound for the witness formula check · The SAT verifier · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · The clause check on the occurrence table is the formula check · The SAT verifier's answer through the occurrence table

DefinitionThe SAT verifier#✓fully proved

The SAT verifier takes a pair \((x, w)\) of lists of Booleans, an input \(x\) and a witness \(w\), and returns a Boolean together with a declared time cost. If the complete CNF decoder fails on \(x\), it returns false at cost \(0\). If \(x\) decodes to a CNF formula \(\varphi\), it returns the result and the cost of the CNF check of \(\varphi\) against the witness \(w\) and the occurrence list of \(\varphi\), so that \(w\) is read as values for the variables of \(\varphi\) in order of occurrence.

Decoding the input is uncharged preprocessing: it adds nothing to the declared cost.

def satVerifier : List Bool × List Bool → TimeM Nat Bool := fun xw =>
  match decodeCNF xw.1 with
  | none => pure false
  | some φ => checkCNF (varsOf φ) xw.2 φ

Uses 4 · Used by 12

Statement usesFormula check against a witness · Decoding a complete length-prefixed CNF formula · Occurrence list of a CNF formula · CNF formula

Used byPreimage of SAT under a polynomial-time map is in NP · Cook–Levin for binary-index CNF-SAT, given a polynomial-time verifier · SAT is in NP if its verifier is polynomial-time · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · Declared time bound of the SAT verifier · The SAT verifier has polynomial declared time · The SAT verifier verifies SAT · The SAT verifier's answer through the occurrence table · The SAT verifier is polynomial-time · Answer of the SAT host with the three-literal filter · 3SAT is in NP

TheoremCost bound for witness lookup#✓fully proved

For every list \(N\) of natural numbers, every list \(w\) of booleans and every natural number \(x\), the cost of looking up \(x\) in \(N\) and \(w\) is at most the length of \(N\).

theorem lookupVar_time_le (ns : List Nat) (bs : List Bool) (x : Nat) :
    (lookupVar ns bs x).time ≤ ns.length

Uses 1 · Used by 1

Statement usesWitness lookup

Used byCost bound for the witness clause check

TheoremLookup in the witness of an assignment#✓fully proved

Let \(v\) be a function from the natural numbers to the booleans, \(N = (n_1, \dots, n_k)\) a list of natural numbers and \(x\) a natural number. Looking up \(x\) in \(N\) and the list \((v(n_1), \dots, v(n_k))\) returns \(v(x)\) if \(x\) occurs in \(N\), and false otherwise.

theorem lookupVar_ret_map (v : Nat → Bool) (ns : List Nat) (x : Nat) :
    (lookupVar ns (ns.map v) x).ret = if x ∈ ns then v x else false

Uses 1 · Used by 1

Statement usesWitness lookup

Used byThe SAT verifier verifies SAT

TheoremCorrectness of the witness clause check#✓fully proved

Let \(N\) be a list of natural numbers, \(w\) a list of booleans and \(C\) a CNF clause. The check of \(C\) against \(N\) and \(w\) returns true if and only if \(C\) is satisfied by the assignment that sends each natural number \(x\) to the value returned by looking up \(x\) in \(N\) and \(w\).

theorem checkClause_ret (vars : List Nat) (w : List Bool) (C : CNFClause) :
    (checkClause vars w C).ret = true ↔
      C.Satisfies (fun x => (lookupVar vars w x).ret)

Uses 4 · Used by 1

Statement usesClause check against a witness · Witness lookup · CNF clause · Satisfaction of a clause

Used byCorrectness of the witness formula check

TheoremCost bound for the witness clause check#✓fully proved

Let \(N\) be a list of natural numbers, \(w\) a list of booleans and \(C\) a CNF clause, viewed as a list of \(\ell\) literals (repetitions counted). The cost of checking \(C\) against \(N\) and \(w\) is at most \(\ell \cdot (|N| + 1)\), where \(|N|\) is the length of \(N\).

Each literal examined costs one tick plus one lookup, and a lookup costs at most \(|N|\).

theorem checkClause_time_le (vars : List Nat) (w : List Bool)
    (C : CNFClause) :
    (checkClause vars w C).time ≤ C.length * (vars.length + 1)

Uses 4 · Used by 1

Statement usesClause check against a witness · CNF clause

Proof usesWitness lookup · Cost bound for witness lookup

Used byCost bound for the witness formula check

TheoremCorrectness of the witness formula check#✓fully proved

Let \(N\) be a list of natural numbers, \(w\) a list of booleans and \(\varphi\) a CNF formula. The check of \(\varphi\) against \(N\) and \(w\) returns true if and only if \(\varphi\) is satisfied by the assignment that sends each natural number \(x\) to the value returned by looking up \(x\) in \(N\) and \(w\).

theorem checkCNF_ret (vars : List Nat) (w : List Bool) (φ : CNF) :
    (checkCNF vars w φ).ret = true ↔
      φ.Satisfies (fun x => (lookupVar vars w x).ret)

Uses 8 · Used by 3

Statement usesFormula check against a witness · Witness lookup · CNF formula · Satisfaction of a CNF formula

Proof usesClause check against a witness · Correctness of the witness clause check · CNF clause · Satisfaction of a clause

Used byPreimage of SAT under a polynomial-time map is in NP · The SAT verifier verifies SAT · The clause check on the occurrence table is the formula check

TheoremCost bound for the witness formula check#✓fully proved

Let \(N\) be a list of natural numbers, \(w\) a list of booleans and \(\varphi\) a CNF formula, and let \(L\) be the sum of the lengths of the clauses of \(\varphi\) (its total number of literals). The cost of checking \(\varphi\) against \(N\) and \(w\) is at most \(L \cdot (|N| + 1)\), where \(|N|\) is the length of \(N\).

theorem checkCNF_time_le (vars : List Nat) (w : List Bool) (φ : CNF) :
    (checkCNF vars w φ).time ≤
      (φ.map List.length).sum * (vars.length + 1)

Uses 5 · Used by 1

Statement usesFormula check against a witness · CNF formula

Proof usesClause check against a witness · Cost bound for the witness clause check · CNF clause

Used byDeclared time bound of the SAT verifier

TheoremLength of the occurrence list#✓fully proved

For every CNF formula \(\varphi\), the length of the occurrence list of \(\varphi\) equals the total number of literals of \(\varphi\), that is, the sum over the clauses of \(\varphi\) of their lengths.

theorem varsOf_length (φ : CNF) :
    (varsOf φ).length = (φ.map List.length).sum

Uses 3 · Used by 2

Statement usesOccurrence list of a CNF formula · CNF formula

Proof usesCNF clause

Used byDeclared time bound of the SAT verifier · The SAT verifier verifies SAT

TheoremVariables of a formula occur in its occurrence list#✓fully proved

Let \(\varphi\) be a CNF formula, \(C\) a clause of \(\varphi\) and \((x, b)\) a literal of \(C\). Then \(x\) belongs to the list of variables occurring in \(\varphi\).

theorem mem_varsOf {x : Nat} {b : Bool} {C : CNFClause} {φ : CNF}
    (hC : (x, b) ∈ C) (hφ : C ∈ φ) : x ∈ varsOf φ

Uses 3 · Used by 2

Statement usesOccurrence list of a CNF formula · CNF formula · CNF clause

Used byThe SAT verifier verifies SAT · Satisfiable formulas give Hamiltonian paths (SAT ≤ HAMPATH, forward direction)

TheoremThe literal count is at most the code length#✓fully proved

For every CNF formula \(\varphi\), the sum over the clauses of \(\varphi\) of their lengths (the total number of literals of \(\varphi\)) is at most the length of the length-prefixed binary code of \(\varphi\).

Each encoded clause contributes at least its literal count.

theorem sum_length_le_encodeCNF_length (φ : CNF) :
    (φ.map List.length).sum ≤ (encodeCNF φ).length

Uses 7 · Used by 2

Statement usesLength-prefixed binary code of a CNF formula · CNF formula

Proof usesLength-prefixed binary code of a clause · Binary code of a literal · Prefix-free code of a natural number · CNF clause · Self-delimiting form of a bitstring

Used byDeclared time bound of the SAT verifier · The SAT verifier verifies SAT

TheoremThe SAT verifier rejects undecodable inputs#✓fully proved

For all lists of Booleans \(x\) and \(w\), if the complete CNF decoder fails on \(x\), then the SAT verifier on \((x, w)\) returns false at declared time cost \(0\).

theorem satVerifier_none {x w : List Bool} (h : decodeCNF x = none) :
    satVerifier (x, w) = pure false

Uses 5 · Used by 4

Statement usesDecoding a complete length-prefixed CNF formula · The SAT verifier · CNF formula

Proof usesFormula check against a witness · Occurrence list of a CNF formula

Used byPreimage of SAT under a polynomial-time map is in NP · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · The SAT verifier's answer through the occurrence table

TheoremThe SAT verifier on a decodable input#✓fully proved

For all lists of Booleans \(x\) and \(w\) and every CNF formula \(\varphi\), if the complete CNF decoder returns \(\varphi\) on \(x\), then the SAT verifier on \((x, w)\) coincides with the CNF check of \(\varphi\) against the witness \(w\) and the occurrence list of \(\varphi\): both the returned Boolean and the declared time cost are the same.

theorem satVerifier_some {x w : List Bool} {φ : CNF}
    (h : decodeCNF x = some φ) :
    satVerifier (x, w) = checkCNF (varsOf φ) w φ

Uses 5 · Used by 4

Statement usesFormula check against a witness · Decoding a complete length-prefixed CNF formula · The SAT verifier · Occurrence list of a CNF formula · CNF formula

Used byPreimage of SAT under a polynomial-time map is in NP · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · The SAT verifier's answer through the occurrence table

TheoremDeclared time bound of the SAT verifier#✓fully proved

For all lists of Booleans \(x\) (the input) and \(w\) (the witness), the declared time cost of the SAT verifier on \((x, w)\) is at most \(N^2 + N\), where \(N = |x| + |w|\) is the sum of their lengths.

If \(x\) decodes to a formula with \(n\) literals, then \(n \le N\) and the check costs at most \(n(n + 1) \le N(N + 1)\).

theorem satVerifier_time_le (xw : List Bool × List Bool) :
    (satVerifier xw).time ≤
      (Polynomial.X ^ 2 + Polynomial.X).eval
        (xw.1.length + xw.2.length)

Uses 12 · Used by 1

Statement usesThe SAT verifier

Proof usesFormula check against a witness · Cost bound for the witness formula check · Decoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · The literal count is at most the code length · Occurrence list of a CNF formula · Length of the occurrence list · CNF formula

Used byThe SAT verifier has polynomial declared time

TheoremThe SAT verifier has polynomial declared time#✓fully proved

There is a polynomial \(q\) with natural number coefficients such that for all lists of Booleans \(x\) (the input) and \(w\) (the witness), the declared time cost of the SAT verifier on \((x, w)\) is at most \(q(|x| + |w|)\).

One can take \(q = X^2 + X\). This bounds only the trusted cost annotation.

theorem satVerifier_verifierInDeclaredPolyTime :
    Cslib.TimeMComplexity.VerifierInDeclaredPolyTime satVerifier

Uses 3

Statement usesThe SAT verifier · Verifiers with polynomial declared time

Proof usesDeclared time bound of the SAT verifier

TheoremThe SAT verifier verifies SAT#✓fully proved

The SAT verifier verifies the SAT decision problem with witness bound the polynomial \(X\): for every list \(x\) of Booleans, \(x\) encodes a satisfiable CNF formula if and only if there is a list \(w\) of Booleans, of length at most the length of \(x\), such that the SAT verifier on \((x, w)\) returns true.

The intended witness lists values for the variables occurring in the decoded formula, in order of occurrence; its length is the literal count, which is at most the input length.

theorem satVerifier_verifies :
    Cslib.TimeMComplexity.Verifies satVerifier satDec Polynomial.X

Uses 36 · Used by 3

Statement usesSAT as a decision problem · The SAT verifier · Verifying a decision problem with a witness bound

Proof usesThe SAT language · Formula check against a witness · Correctness of the witness formula check · Decoding a complete length-prefixed CNF formula · Decoding a length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Decoding a length-prefixed clause · Decoding a fixed number of clauses · Decoding a literal · Decoding a fixed number of literals · Decoding a prefix-coded natural number · Length-prefixed binary code of a CNF formula · Length-prefixed binary code of a clause · Binary code of a literal · Prefix-free code of a natural number · Witness lookup · Lookup in the witness of an assignment · Variables of a formula occur in its occurrence list · Reading a unary length prefix · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · The literal count is at most the code length · Occurrence list of a CNF formula · Length of the occurrence list · CNF formula · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Satisfiability of a CNF formula · Satisfiability means having a satisfying assignment · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Used byPreimage of SAT under a polynomial-time map is in NP · SAT is in NP if its verifier is polynomial-time · 3SAT is in NP

TheoremSAT is in NP if its verifier is polynomial-time#✓fully proved

If the function sending a pair \((x, w)\) of lists of Booleans to the Boolean returned by the SAT verifier on \((x, w)\) is polynomial-time computable, by a multi-stack Turing machine under the canonical bitstring encodings, then the SAT decision problem belongs to NP.

This hypothesis must be proved separately: it does not follow from the polynomial bound on the SAT verifier's declared time, which constrains only a trusted cost annotation and leaves the decoding of the input uncharged.

theorem satDec_mem_NP_of_isPolyTime
    (h : MetaMathlibExt.ComplexityTheory.IsPolyTime
      fun xw => (satVerifier xw).ret) :
    satDec ∈ MetaMathlibExt.ComplexityTheory.NP

Uses 16 · Used by 2

Statement usesSAT as a decision problem · The SAT verifier · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Complexity classes · Decision problems · Polynomial-time computable functions · The complexity class NP

Proof usesThe SAT verifier verifies SAT · A timed verifier with polynomial-time output function puts its language in NP

Used byCook–Levin for binary-index CNF-SAT, given a polynomial-time verifier · SAT is in NP

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.