Binary encoding of CNF formulas

DefinitionReading a unary length prefix#✓fully proved

On a list of Booleans that begins with \(k\) copies of \(\mathrm{true}\) followed by \(\mathrm{false}\), the reader returns \(k\) together with the rest of the list after that \(\mathrm{false}\). On a list containing no \(\mathrm{false}\), including the empty list, it fails.

def readUnaryLength : List Bool → Option (Nat × List Bool)
  | [] => none
  | false :: rest => some (0, rest)
  | true :: rest => (readUnaryLength rest).map fun result => (result.1 + 1, result.2)

Used by 68

Used byDecoding a list of cells · Cell-by-cell check of a code stack · The cell-by-cell check recognizes code stacks · Decoding inverts the code stack · Code stacks are recognized · Code stacks, entry by entry · Reading a unary length prefix reads one cell · The checking run · Decoding a length-prefixed clause · The CNF decoder inverts the length-prefixed CNF code · Decoding a length-prefixed CNF formula · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Tokenizer rejects undecodable clauses · Rejecting run · An unterminated unary count is rejected · 3SAT is in NP · Decoding a graph · Edge-list decoder · Decoding the empty input · The edge-list decoder fails on a cut-off first number · Decoding fails on a dangling half-pair · Reading a unary number shortens the input · Graph decoding inverts graph encoding · Decoding the bits of an edge list · Decoding one pair, then the rest · The edge-list decoder succeeds only on edge bits · Graph decoding succeeds only on encodings · Correctness of the SAT to 3-COLOR map on bit strings · The 3-COLOR verifier as an edge loop · Edge-loop verdict after one parsed edge · Correctness and running time of the edge loop · The unary reader rejects an unterminated number · Correctness and time bound of the 3-coloring verifier machine · Decoding a graph instance · Unparsable input is rejected · Correctness of the complementing map from CLIQUE to INDEPENDENT-SET · Characterization of the CLIQUE verifier · Reading an unterminated unary number rejects · The verifier machine for clique, independent set and vertex cover · Unterminated first unary number in the KG-map machine · Unterminated second unary number in the KG-map machine · Correctness and running time of the KG-map machine · CLIQUE is NP-hard · VERTEX-COVER (exact size k) is NP-hard · Subset-sum emitter: unterminated unary prefix at rdK · Subset-sum emitter: unterminated unary prefix at rdN · Run of the VERTEX-COVER to SUBSET-SUM machine · SUBSET-SUM is NP-hard · Witness decoder · Decoding inverts the witness encoding · Decoding the empty witness · Witness decoding fails on a cut-off first number · Decoding peels off the first number · The witness decoder succeeds only on encodings · The unary reader of the Hamiltonian path verifier rejects an unterminated number · The unary mover of the Hamiltonian path verifier rejects an unterminated number · The edge-list check of the Hamiltonian-path verifier · The witness check of the Hamiltonian-path verifier · Correctness and running time of the Hamiltonian path verifier · Correctness of the SAT-to-3SAT reduction on bit strings · Decoding a PATH instance · Decoding inverts the PATH instance encoding · The PATH instance parser succeeds exactly on encodings · Reading a cut-off unary number · Running time and output of the marking machine · Validation phase of the PATH marking machine

DefinitionPrefix-free code of a natural number#✓fully proved

The code of \(n \in \mathbb{N}\) is the self-delimiting block of the binary representation of \(n\) (least significant bit first, with \(0\) represented by the empty list): each bit \(c\) is written as the two bits \(\mathrm{true}, c\), and the block ends with a terminating \(\mathrm{false}\).

def encodeNatPrefix (n : Nat) : List Bool :=
  MetaMathlibExt.BitstringEncoding.delimit (Computability.encodeNat n)

Uses 1 · Used by 20

Statement usesSelf-delimiting form of a bitstring

Used byThe CNF decoder inverts the length-prefixed CNF code · Binary code of a literal · Binary codes of literals on variables one less than a power of two · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · The literal count is at most the code length · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer rejects undecodable literals · Reading the literals of a clause · Rejecting run · 3SAT is in NP · Decoding a SUBSET-SUM instance inverts its encoding · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum · Code of a fresh literal · Code of a renamed literal · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionDecoding a prefix-coded natural number#✓fully proved

Given a bit string \(w\), writing \(1\) for true and \(0\) for false, the decoder reads one self-delimiting block \(1\,b_1\,1\,b_2 \cdots 1\,b_k\,0\) from the front of \(w\), with payload \(b_1 \cdots b_k\) and remaining bits \(r\). If the payload is the binary expansion of some natural number \(n\), least significant bit first and without trailing zeros (empty for \(n = 0\)), the result is \((n, r)\). Decoding fails if \(w\) does not begin with such a block or the payload is not of this form.

def decodeNatPrefix (input : List Bool) : Option (Nat × List Bool) := do
  let (bits, rest) ← MetaMathlibExt.BitstringEncoding.undelimit input
  let n := Computability.decodeNat bits
  if Computability.encodeNat n = bits then some (n, rest) else none

Uses 1 · Used by 17

Statement usesParsing one self-delimiting block

Used byThe CNF decoder inverts the length-prefixed CNF code · Decoding a literal · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Tokenizer rejects undecodable clauses · Tokenizer rejects an undecodable literal · Tokenizer rejects undecodable literals · Rejecting run · 3SAT is in NP · Decoding a SUBSET-SUM instance · Decoding a SUBSET-SUM instance inverts its encoding · Parsing number blocks, with fuel · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionBinary code of a literal#✓fully proved

A literal \((n, b)\), with variable index \(n \in \mathbb{N}\) and polarity \(b \in \{\mathrm{false}, \mathrm{true}\}\), is encoded as the prefix-free code of \(n\) followed by the single bit \(b\).

def encodeLit (l : Nat × Bool) : List Bool :=
  encodeNatPrefix l.1 ++ [l.2]

Uses 1 · Used by 28

Statement usesPrefix-free code of a natural number

Used byThe CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a clause · The translation on a whole clause · The translation on the remaining clauses · The translation computes the binary encoding · The translation on the slots of a clause · Binary codes of literals on variables one less than a power of two · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · The literal count is at most the code length · A clause has at most as many tokens as code bits · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on one literal · Tokenizer rejects undecodable literals · Reading the literals of a clause · Rejecting run · 3SAT is in NP · The 3SAT emitter processes one clause · Code of a fresh literal · Code of a renamed literal · Fresh-literal subroutine of the 3SAT emitter · The 3SAT emitter reads a literal marker · One literal of the emitter · Copying a renamed name · Correctness of the SAT-to-3SAT reduction on bit strings · Closing an output clause in the SAT-to-3SAT emitter

DefinitionDecoding a literal#✓fully proved

Given a bit string \(w\), the decoder reads a prefix-coded natural number \(n\) from the front of \(w\) and then one more bit \(b\). The result is the literal \((n, b)\), with variable index \(n\) and polarity \(b\), together with the bits left after \(b\). Decoding fails if no prefix-coded natural number can be read or no bit follows it.

def decodeLit (input : List Bool) : Option ((Nat × Bool) × List Bool) := do
  let (n, rest) ← decodeNatPrefix input
  match rest with
  | [] => none
  | polarity :: tail => some ((n, polarity), tail)

Uses 1 · Used by 11

Statement usesDecoding a prefix-coded natural number

Used byThe CNF decoder inverts the length-prefixed CNF code · Decoding a fixed number of literals · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Tokenizer rejects undecodable clauses · Tokenizer rejects an undecodable literal · Tokenizer rejects undecodable literals · Rejecting run · 3SAT is in NP · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionDecoding a fixed number of literals#✓fully proved

For a natural number \(n\) and a bit string \(w\), the decoder reads \(n\) literals one after another from the front of \(w\) with the literal decoder. The result is the clause made of these literals, in order, together with the bits left after them; for \(n = 0\) it is the empty clause together with \(w\). Decoding fails if one of the \(n\) literals cannot be read.

def decodeLits : Nat → List Bool → Option (CNFClause × List Bool)
  | 0, input => some ([], input)
  | n + 1, input => do
      let (literal, rest) ← decodeLit input
      let (literals, tail) ← decodeLits n rest
      some (literal :: literals, tail)

Uses 2 · Used by 10

Statement usesDecoding a literal · CNF clause

Used byDecoding a length-prefixed clause · The CNF decoder inverts the length-prefixed CNF code · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Tokenizer rejects undecodable clauses · Tokenizer rejects undecodable literals · Rejecting run · 3SAT is in NP · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionLength-prefixed binary code of a clause#✓fully proved

Writing \(1\) for true and \(0\) for false, the code of a clause \(C = (\ell_1, \dots, \ell_k)\) is \(1^k 0\) (\(k\) ones followed by a zero) followed by the binary codes of \(\ell_1, \dots, \ell_k\) in order, where a literal \((x, b)\) with variable index \(x\) and polarity \(b\) is coded by the prefix-free code of \(x\) followed by the bit \(b\).

def encodeClause (C : CNFClause) : List Bool :=
  List.replicate C.length true ++ false :: C.flatMap encodeLit

Uses 2 · Used by 24

Statement usesBinary code of a literal · CNF clause

Used byThe CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · The translation on the remaining clauses · The translation computes the binary encoding · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · The literal count is at most the code length · A clause has at most as many tokens as code bits · Token count is bounded by the encoding length · Tokenizer run on one clause · Tokenizer rejects undecodable clauses · Tokenizer run on all clauses · Rejecting run · Accepting run of the SAT tokenizer · Clause token length bound for the SAT verifier (moved alias) · 3SAT is in NP · The 3SAT emitter processes one clause · CNF encodings are nonempty · The 3SAT emitter processes a whole formula · One literal of the emitter · The literals of a clause in the emitter · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionDecoding a length-prefixed clause#✓fully proved

Given a bit string \(w\), writing \(1\) for true and \(0\) for false, the decoder reads a unary length prefix \(1^n 0\) (\(n\) ones followed by a zero) from the front of \(w\), then reads exactly \(n\) literals from the remaining bits with the literal decoder. The result is the clause made of these literals, in order, together with the bits left after them. Decoding fails if \(w\) does not begin with such a prefix or one of the literals cannot be read.

def decodeClause (input : List Bool) : Option (CNFClause × List Bool) := do
  let (n, rest) ← readUnaryLength input
  decodeLits n rest

Uses 3 · Used by 9

Statement usesDecoding a fixed number of literals · Reading a unary length prefix · CNF clause

Used byDecoding a fixed number of clauses · The CNF decoder inverts the length-prefixed CNF code · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Tokenizer rejects undecodable clauses · Rejecting run · 3SAT is in NP · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionDecoding a fixed number of clauses#✓fully proved

For a natural number \(n\) and a bit string \(w\), the decoder reads \(n\) clauses one after another from the front of \(w\) with the length-prefixed clause decoder. The result is the CNF formula made of these clauses, in order, together with the bits left after them; for \(n = 0\) it is the empty formula together with \(w\). Decoding fails if one of the \(n\) clauses cannot be read.

def decodeClauses : Nat → List Bool → Option (CNF × List Bool)
  | 0, input => some ([], input)
  | n + 1, input => do
      let (clause, rest) ← decodeClause input
      let (clauses, tail) ← decodeClauses n rest
      some (clause :: clauses, tail)

Uses 3 · Used by 9

Statement usesDecoding a length-prefixed clause · CNF formula · CNF clause

Used byThe CNF decoder inverts the length-prefixed CNF code · Decoding a length-prefixed CNF formula · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Tokenizer rejects undecodable clauses · Rejecting run · 3SAT is in NP · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionLength-prefixed binary code of a CNF formula#✓fully proved

Writing \(1\) for true and \(0\) for false, the code of a CNF formula \(\varphi = (C_1, \dots, C_m)\) is \(1^m 0\) (\(m\) ones followed by a zero) followed by the length-prefixed binary codes of the clauses \(C_1, \dots, C_m\) in order.

def encodeCNF (φ : CNF) : List Bool :=
  List.replicate φ.length true ++ false :: φ.flatMap encodeClause

Uses 3 · Used by 27

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

Used byPreimage of SAT under a polynomial-time map is in NP · The CNF decoder inverts the length-prefixed CNF code · Encodings of satisfiable CNF formulas · The translation computes the binary encoding · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · Every NP problem reduces to binary-index CNF-SAT · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · The literal count is at most the code length · Token count is bounded by the encoding length · Rejecting run · Accepting run of the SAT tokenizer · The TM2 SAT verifier · 3SAT is in NP · Token length bound for the SAT verifier (moved alias) · Correctness of the SAT to 3-COLOR map on bit strings · CLIQUE is NP-hard · SAT ≤ HAMPATH preserves membership · The SAT-to-3SAT emitter · CNF encodings are nonempty · The SAT-to-3SAT reduction is polynomial-time · The SAT-to-3SAT reduction on bit strings · The SAT-to-3SAT emitter writes the encoded translation in quadratic time · Tokenize, then emit · Correctness of the SAT-to-3SAT reduction on bit strings · The 3SAT decision problem

DefinitionDecoding a length-prefixed CNF formula#✓fully proved

Given a bit string \(w\), writing \(1\) for true and \(0\) for false, the decoder reads a unary length prefix \(1^n 0\) (\(n\) ones followed by a zero) from the front of \(w\), then reads exactly \(n\) clauses from the remaining bits with the length-prefixed clause decoder. The result is the CNF formula made of these clauses, in order, together with the bits left after them. Decoding fails if \(w\) does not begin with such a prefix or one of the clauses cannot be read.

def decodeCNFAux (input : List Bool) : Option (CNF × List Bool) := do
  let (n, rest) ← readUnaryLength input
  decodeClauses n rest

Uses 3 · Used by 8

Statement usesDecoding a fixed number of clauses · Reading a unary length prefix · CNF formula

Used byDecoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Rejecting run · 3SAT is in NP · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionDecoding a complete length-prefixed CNF formula#✓fully proved

Given a bit string \(w\), the decoder reads one CNF formula \(\varphi\) from the front of \(w\) with the length-prefixed CNF decoder, which also returns the bits left after \(\varphi\). The result is \(\varphi\) if no bits are left; decoding fails if no formula can be read or if bits remain after it.

def decodeCNF (input : List Bool) : Option CNF := do
  let (φ, rest) ← decodeCNFAux input
  if rest.isEmpty then some φ else none

Uses 2 · Used by 33

Statement usesDecoding a length-prefixed CNF formula · CNF formula

Used byPreimage of SAT under a polynomial-time map is in NP · The CNF decoder inverts the length-prefixed CNF code · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · 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 SAT verifier's answer through the occurrence table · Tokenizer of the SAT verifier · Rejecting run · Accepting run of the SAT tokenizer · Answer of the SAT host · The SAT verifier is polynomial-time · The TM2 SAT verifier · Answer of the SAT host with the three-literal filter · 3SAT is in NP · The SAT to 3-COLOR reduction map on bit strings · Correctness of the SAT to 3-COLOR map on bit strings · The SAT-to-3-COLOR reduction is polynomial-time · Karp's SAT-to-CLIQUE map on bit strings · SAT decision on undecodable input (moved alias) · SAT ≤ CLIQUE is polynomial-time · CLIQUE is NP-hard · The SAT-to-HAMPATH reduction map · SAT ≤ HAMPATH preserves membership · SAT ≤ HAMPATH is polynomial-time · The SAT-to-3SAT reduction is polynomial-time · Output of an emitter on a bit string · The SAT-to-3SAT reduction on bit strings · Tokenize, then emit · Correctness of the SAT-to-3SAT reduction on bit strings

TheoremParsing a self-delimiting block#✓fully proved

For all lists of Booleans \(u\), \(p\) and \(r\), parsing one self-delimiting block from the front of \(u\) succeeds with payload \(p\) and remainder \(r\) if and only if \(u\) is the self-delimiting block of \(p\) followed by \(r\).

theorem undelimit_eq_some_iff (input bits rest : List Bool) :
    MetaMathlibExt.BitstringEncoding.undelimit input = some (bits, rest) ↔
      input = MetaMathlibExt.BitstringEncoding.delimit bits ++ rest

Uses 2 · Used by 19

Statement usesSelf-delimiting form of a bitstring · Parsing one self-delimiting block

Used byThe CNF decoder inverts the length-prefixed CNF code · List canonicalizer fails on malformed input · Pair-list projector fails on malformed input in linear time · Successful block parsing reconstructs the input · Frame counter fails on malformed list framing · Four-output decoder fails on malformed input · Raw field projection agrees with the pair decoder · Pair-frame splitter projects every well-framed input in linear time · Decoded block count is at most the input length · Decoded pair exposes its raw component payloads · Parsing a framed head leaves the raw remainder · Tokenizer rejects undecodable clauses · Tokenizer rejects an undecodable literal · Tokenizer rejects undecodable literals · Rejecting run · Decoding a SUBSET-SUM instance inverts its encoding · The summing loop of the SUBSET-SUM verifier · The SUBSET-SUM verifier machine · SUBSET-SUM verifier computes the mask-selected sum

TheoremThe CNF decoder inverts the length-prefixed CNF code#✓fully proved

For every bit string \(w\) and every CNF formula \(\varphi\), the complete CNF decoder returns \(\varphi\) on input \(w\) if and only if \(w\) is the length-prefixed binary code of \(\varphi\).

@[simp] theorem decodeCNF_eq_some_iff (input : List Bool) (φ : CNF) :
    decodeCNF input = some φ ↔ input = encodeCNF φ

Uses 17 · Used by 11

Statement usesDecoding a complete length-prefixed CNF formula · Length-prefixed binary code of a CNF formula · CNF formula

Proof usesDecoding a length-prefixed CNF formula · 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 clause · Binary code of a literal · Prefix-free code of a natural number · Reading a unary length prefix · Parsing a self-delimiting block · CNF clause · Self-delimiting form of a bitstring · Parsing one self-delimiting block

Used byPreimage of SAT under a polynomial-time map is in NP · Declared time bound of the SAT verifier · The SAT verifier verifies SAT · Accepting run of the SAT tokenizer · The TM2 SAT verifier · 3SAT is in NP · Correctness of the SAT to 3-COLOR map on bit strings · CLIQUE is NP-hard · SAT ≤ HAMPATH preserves membership · Tokenize, then emit · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionEncodings of satisfiable CNF formulas#✓fully proved

A list \(x\) of Booleans encodes a satisfiable CNF formula when \(x\) is the binary code of some CNF formula \(\varphi\) and \(\varphi\) is satisfiable.

def IsSATEncoded (x : List Bool) : Prop :=
  ∃ φ : CNF, encodeCNF φ = x ∧ CNFSat φ

Uses 3 · Used by 1

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

Used byThe SAT language

DefinitionThe SAT language#✓fully proved

SAT is the set of lists of Booleans that encode a satisfiable CNF formula.

def SATLang : Set (List Bool) :=
  {x | IsSATEncoded x}

Uses 1 · Used by 5

Statement usesEncodings of satisfiable CNF formulas

Used bySAT as a decision problem · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · The SAT verifier verifies SAT · Correctness of the SAT-to-3SAT reduction on bit strings

DefinitionSAT as a decision problem#✓fully proved

The SAT decision problem returns true on a list \(x\) of Booleans when \(x\) lies in the SAT language, that is, when \(x\) encodes a satisfiable CNF formula, and false otherwise.

noncomputable def satDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x => if x ∈ SATLang then true else false

Uses 2 · Used by 21

Statement usesThe SAT language · Decision problems

Used byNP is closed under polynomial-time preimages · Preimage of SAT under a polynomial-time map is in NP · Cook–Levin theorem: SAT is NP-complete · SAT accepts the code of a formula exactly when it is satisfiable · Unparsable input is not in SAT · Cook–Levin for binary-index CNF-SAT, given a polynomial-time verifier · Every NP problem reduces to binary-index CNF-SAT · SAT is in NP if its verifier is polynomial-time · The SAT verifier verifies SAT · SAT is in NP · Cook–Levin theorem · 3SAT is in NP · Correctness of the SAT to 3-COLOR map on bit strings · 3-COLOR is NP-hard · SAT decision on undecodable input (moved alias) · CLIQUE is NP-hard · SAT ≤ HAMPATH preserves membership · HAMPATH is NP-hard · Correctness of the SAT-to-3SAT reduction on bit strings · SAT reduces to 3SAT · 3SAT is NP-hard

DefinitionPolynomial-time many-one reduction#✓fully proved

A decision problem \(L_1\) reduces to a decision problem \(L_2\) in polynomial time when there is a polynomial-time computable function \(f\) from lists of Booleans to lists of Booleans such that \(L_1(x) = L_2(f(x))\) for every list \(x\) of Booleans.

def PolyManyOneRed (L₁ L₂ : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
  ∃ reduce : List Bool → List Bool,
    MetaMathlibExt.ComplexityTheory.IsPolyTime reduce ∧ ∀ x, L₁ x = L₂ (reduce x)

Uses 10 · Used by 141

Statement usesBitstring 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 · Decision problems · Polynomial-time computable functions

Used byGeography is PSPACE-complete · \(\mathrm{QSAT}_k\) is \(\Sigma_k^p\)-complete, uniformly in \(k\) · Regular expressions with squaring: universality is EXPSPACE-complete · The model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete · Satisfiability of a modal μ-calculus formula is EXPTIME-complete · Succinct 3SAT is NEXP-complete · Succinct Circuit Value is EXP-complete · TQBF is PSPACE-complete · UNSAT is coNP-complete · Ladner's theorem: NP-intermediate languages exist · NP-complete decision problems · From declared-time to polynomial-time many-one reductions · NP is closed under polynomial-time preimages · Polynomial many-one reductions also reduce complements · NP membership pulls back along polynomial many-one reductions · MAJSAT is PP-complete · Cook-Levin for dense CNF-SAT · Every NP problem reduces to dense CNF-SAT · Cook–Levin theorem: SAT is NP-complete · Cook–Levin for binary-index CNF-SAT, given a polynomial-time verifier · Every NP problem reduces to binary-index CNF-SAT · Cook–Levin theorem · ACHROMATIC NUMBER is NP-complete · EDGE COLORING is NP-complete · 3-COLOR is NP-complete · 3-COLOR is NP-hard · BANDWIDTH is NP-complete · GRAPH COLORING is NP-complete · GRAPH HOMOMORPHISM is NP-complete · LINEAR ORDERING (TOURNAMENTS) is NP-complete · LIST COLORING is NP-complete · MAXIMUM CUT is NP-complete · MAXIMUM k-CUT is NP-complete · MINIMUM BISECTION is NP-complete · MINIMUM LINEAR ARRANGEMENT is NP-complete · MULTIWAY CUT is NP-complete · PARTITION INTO PATHS OF LENGTH 2 is NP-complete · PARTITION INTO TRIANGLES is NP-complete · PRECOLORING EXTENSION is NP-complete · BALANCED BICLIQUE is NP-complete · BICLIQUE EDGE COVER is NP-complete · CLIQUE is NP-complete · CLIQUE is NP-hard · INDEPENDENT-SET is NP-complete · INDEPENDENT-SET is NP-hard · VERTEX-COVER (exact size k) is NP-complete · VERTEX-COVER (exact size k) is NP-hard · CONNECTED DOMINATING SET is NP-complete · DENSEST k-SUBGRAPH is NP-complete · DOMINATING SET is NP-complete · EDGE DOMINATING SET is NP-complete · EFFICIENT DOMINATION (PERFECT CODE) is NP-complete · FEEDBACK ARC SET is NP-complete · FEEDBACK VERTEX SET is NP-complete · INDEPENDENT DOMINATING SET is NP-complete · MAXIMUM INDUCED MATCHING is NP-complete · MINIMUM FILL-IN (CHORDAL COMPLETION) is NP-complete · ODD CYCLE TRANSVERSAL is NP-complete · ROMAN DOMINATION is NP-complete · TOTAL DOMINATING SET is NP-complete · 0-1 INTEGER PROGRAMMING FEASIBILITY is NP-complete · 3-PARTITION is NP-complete · BIN PACKING is NP-complete · EXACT-CARDINALITY SUBSET SUM is NP-complete · KNAPSACK is NP-complete · MULTIPLE KNAPSACK is NP-complete · MULTIWAY NUMBER PARTITION is NP-complete · NUMERICAL 3-DIMENSIONAL MATCHING is NP-complete · PARTITION is NP-complete · Polynomial-time reduction from SUBSET-SUM to PARTITION · STRIP PACKING is NP-complete · SUBSET PRODUCT is NP-complete · SUBSET-SUM is NP-complete · SUBSET-SUM is NP-hard · UNBOUNDED KNAPSACK is NP-complete · TRAVELING SALESPERSON (ASYMMETRIC) is NP-complete · CAPACITATED VEHICLE ROUTING is NP-complete · DEGREE-CONSTRAINED SPANNING TREE is NP-complete · HAMILTONIAN CYCLE (DIRECTED) is NP-complete · HAMPATH is NP-complete · HAMPATH is NP-hard · INDUCED SUBGRAPH ISOMORPHISM is NP-complete · LONGEST CYCLE is NP-complete · LONGEST PATH is NP-complete · MAXIMUM COMMON INDUCED SUBGRAPH is NP-complete · MAXIMUM LEAF SPANNING TREE is NP-complete · MINIMUM EQUIVALENT DIGRAPH is NP-complete · DIRECTED PATH COVER is NP-complete · STEINER TREE is NP-complete · SUBGRAPH ISOMORPHISM is NP-complete · TRAVELING SALESPERSON (SYMMETRIC) is NP-complete · HAMILTONIAN CYCLE (UNDIRECTED) is NP-complete · HAMILTONIAN PATH (UNDIRECTED) is NP-complete · DIRECTED DISJOINT PATHS is NP-complete · 1-IN-3-SAT is NP-complete · 3-SAT WITH BOUNDED OCCURRENCES is NP-complete · NP-hardness transfers along reductions · Transitivity of polynomial-time many-one reductions · SAT reduces to 3SAT · 3SAT is NP-complete · 3SAT is NP-hard · BETWEENNESS is NP-complete · BINARY CONSTRAINT SATISFACTION is NP-complete · CIRCUIT SAT is NP-complete · MAXIMUM 2-SATISFIABILITY is NP-complete · MAXIMUM SATISFIABILITY is NP-complete · MINIMUM 2-SATISFIABILITY is NP-complete · MINIMUM ONES 3-SAT is NP-complete · MONOTONE 3-SAT is NP-complete · NOT-ALL-EQUAL 3-SAT is NP-complete · JOB SEQUENCING WITH DEADLINES, PROCESSING TIMES, AND PROFITS is NP-complete · PARALLEL MACHINES WITH DEADLINES is NP-complete · PRECEDENCE-CONSTRAINED MULTIPROCESSOR SCHEDULING is NP-complete · RESOURCE-CONSTRAINED PROJECT SCHEDULING is NP-complete · SINGLE-MACHINE SCHEDULING WITH RELEASE TIMES AND DEADLINES is NP-complete · 3-MACHINE FLOW SHOP SCHEDULING is NP-complete · TOTAL TARDINESS is NP-complete · SINGLE-MACHINE WEIGHTED COMPLETION WITH PRECEDENCE is NP-complete · WEIGHTED NUMBER OF TARDY JOBS is NP-complete · 3-DIMENSIONAL MATCHING is NP-complete · EXACT COVER BY 3-SETS is NP-complete · EXACT COVER is NP-complete · FACILITY LOCATION is NP-complete · GENERALIZED ASSIGNMENT is NP-complete · MAXIMUM COVERAGE is NP-complete · MAXIMUM n-TIMES COVERAGE is NP-complete · MINIMUM TEST SET is NP-complete · k-CENTER (GENERALIZED, NONMETRIC) is NP-complete · k-MEDIAN (GENERALIZED, NONMETRIC) is NP-complete · QUADRATIC ASSIGNMENT is NP-complete · SET COVER is NP-complete · SET PACKING is NP-complete · SET SPLITTING is NP-complete · AKARI (LIGHT UP) is NP-complete · CLOSEST STRING is NP-complete · LATIN SQUARE COMPLETION is NP-complete · LONGEST COMMON SUBSEQUENCE is NP-complete · MINESWEEPER CONSISTENCY is NP-complete · NONOGRAM is NP-complete · SHORTEST COMMON SUPERSEQUENCE is NP-complete · SUDOKU is NP-complete

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.