NP-hardness of binary-index SAT

TheoremEvery clause of the Cook–Levin formula has one slot per variable#✓fully proved

Let \(E\) be an encoding of a machine \(M\), let \(x\) and \(Y\) be lists of input symbols of \(M\), let \(a\) be a symbol of its output stack, and let \(m, T \in \mathbb{N}\). Put \(H = m + (T + 1)d + 1\), where \(d\) is the window depth of \(M\). Then every clause of the Cook–Levin formula \(\Phi(E, x, Y, a, m, T)\) is a dense clause of length \((T + 1)(A + K H g)\), the number of variables of the layout of \(E\) at time bound \(T\) and height \(H\), where \(A\), \(K\) and \(g\) are the label/state block size, the number of stacks and the number of symbol codes of that layout.

theorem Phi_length {M : FinTM2} (E : Enc M) (x Ys : List (M.Γ M.k₀)) (acc : M.Γ M.k₁) (m T : ℕ) :
    ∀ c ∈ Phi E x Ys acc m T, c.length = E.layout.numVars T (capH m T (depth M))

Uses 36 · Used by 1

Statement usesThe formula emitted by the host · Number of variables of the transition-clause formula · Encoding data for a finite TM2 machine · Clause layout of a machine encoding · Stack cap · Window depth of a machine · Dense CNF formula · Dense clause

Proof usesVariable layout of the transition clauses · Index of a cell variable in the transition-family layout · Index of a label/state variable · Dense clause from a list of literals · The transition clause family · Literals of a transition clause · Literals of an overflow clause · Literals of a pushed-fill clause · The shift block of a situation and a stack · The cell-shift clause family · Literals of an in-range shift clause · Number of situations · Accepting code · Consumption table of a situation · Symbol-code bound · Certificate clauses of the init family · Start-code clause of the init family · The row-0 init family of an encoding · Input clauses of the init family · Empty-stack clauses of the init family · Prefix clauses of the init family · Label/state code of a situation · Next label/state code of a situation · Push-count table of a situation · Pushed-symbol table of a situation · Position of a situation's variable · Window symbol code of a situation · Index of the empty-cell variable of the input stack

Used byEvery NP problem reduces to binary-index CNF-SAT

TheoremThe dense-to-binary translation is polynomial-time in the canonical encoding#✓fully proved

The translation of bit strings from the dense CNF encoding to the binary-index CNF encoding, as a function on all bit strings, is polynomial-time computable with respect to the canonical bitstring encoding of bit lists.

theorem isPolyTime_binConv : IsPolyTime ToBinary.binConv

Uses 14 · Used by 1

Statement usesThe dense-to-binary translation on bit strings · 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 · Polynomial-time computable functions

Proof usesPolynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · The dense-to-binary translation on raw bits is polynomial-time · Polynomial-time TM2-computable functions are closed under composition

Used byEvery NP problem reduces to binary-index CNF-SAT

TheoremEvery NP problem reduces to binary-index CNF-SAT#✓fully proved

Every decision problem \(L\) in NP has a polynomial-time many-one reduction to the language of bit strings that encode a satisfiable CNF formula in the binary-index encoding.

theorem satDec_npHard (L : DecisionProblem) (hL : L ∈ NP) :
    Cslib.CookLevin.PolyManyOneRed L Cslib.CookLevin.satDec

Uses 54 · Used by 5

Statement usesPolynomial-time many-one reduction · SAT as a decision problem · Complexity classes · Decision problems · The complexity class NP

Proof usesThe formula emitted by the host · Number of variables of the transition-clause formula · Every clause of the Cook–Levin formula has one slot per variable · The dense-to-binary translation is polynomial-time in the canonical encoding · The Cook–Levin reduction is polynomial-time · The Cook–Levin reduction · Tableau encoding of the verifier · Certificate symbols of the verifier · Correctness of the reduction · Accept symbol of the verifier · Offset of the verifier's time bound · Exponent of the verifier's time bound · Bits as indices · Separator symbol of the verifier · Input-bit symbol of the verifier · The Cook–Levin reduction function · The precomputed time bound · Total length bound · Clause layout of a machine encoding · Stack cap · Window depth of a machine · Dense CNF formula · Dense CNF-SAT · Binary-index translation of a dense formula · The dense-to-binary translation on bit strings · The binary-index translation preserves satisfiability when all clauses have equal length · The translation computes the binary encoding · SAT accepts the code of a formula exactly when it is satisfiable · Canonical bit-list decoder · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Satisfaction of a dense CNF formula · Dense decoding of CNF formulas · Decoding inverts the dense encoding · Dense encoding of a CNF formula · Length-prefixed binary code of a CNF formula · CNF formula · Satisfiability of a CNF formula · 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 · Polynomial-time computable functions · Polynomial-time functions are closed under composition · The composite polynomial-time TM2 computation

Used byCook–Levin for binary-index CNF-SAT, given a polynomial-time verifier · 3-COLOR is NP-hard · CLIQUE is NP-hard · HAMPATH is NP-hard · 3SAT is NP-hard

TheoremCook–Levin for binary-index CNF-SAT, given a polynomial-time verifier#✓fully proved

If the Boolean result of the SAT verifier, as a function of pairs (formula code, assignment), is computable in polynomial time, then the language of bit strings that encode a satisfiable CNF formula in the binary-index encoding is in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

theorem cook_levin_SAT_np_complete_of_isPolyTime
    (h : IsPolyTime fun xw => (Cslib.CookLevin.satVerifier xw).ret) :
    Cslib.CookLevin.satDec ∈ NP ∧
      ∀ L : DecisionProblem, L ∈ NP → Cslib.CookLevin.PolyManyOneRed L Cslib.CookLevin.satDec

Uses 17 · Used by 1

Statement usesPolynomial-time many-one reduction · SAT 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 usesEvery NP problem reduces to binary-index CNF-SAT · SAT is in NP if its verifier is polynomial-time

Used byCook–Levin theorem

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.