Succinct 3SAT

AbbreviationEncoded gates#✓fully proved

An encoded gate is a pair \((k, r)\) of a natural number \(k\), the kind of the gate, and a list \(r\) of natural numbers, its references. This is the (kind, references) encoding of the gates of a flat Boolean circuit.

abbrev S3Gate := ℕ × List ℕ
Used by 7
Used byGate values of an encoded circuit · Outputs of an encoded circuit · Valid gates of a succinct 3SAT descriptor · Well-formed succinct 3SAT descriptors · Satisfied clauses of a succinctly described formula · Literals of a succinctly described formula · Succinct 3SAT

DefinitionGate values of an encoded circuit#✓fully proved

Let \(C = (g_0, \dots, g_{m-1})\) be a list of gates, each encoded as a (kind, references) pair, let \(\alpha\) be a list of booleans and let \(n\) be a natural number. The gate values of \(C\) on \(\alpha\) are the values \((v_0, \dots, v_{m-1})\) of the flat Boolean circuit on \(n + 2\) inputs obtained by decoding every \(g_j\), when input \(i\) is given entry \(i\) of \(\alpha\), read as false when \(i\) is at least the length of \(\alpha\).

def s3CircuitEval (C : List S3Gate) (assign : List Bool) (n : ℕ) : List Bool :=
  circuitEval (C.map (acGateOfPair (n := n + 2))) (fun i => assign.getD i.val false)
Uses 4 · Used by 1
Statement usesGates of a flat Boolean circuit · Decoding a gate from its (kind, references) pair · Evaluation of a flat Boolean circuit · Encoded gates
Used byOutputs of an encoded circuit

DefinitionOutputs of an encoded circuit#✓fully proved

Let \(C\) be a list of \(m\) gates encoded as (kind, references) pairs, let \(\alpha\) be a list of booleans and let \(k\) and \(n\) be natural numbers. The last \(k\) outputs of \(C\) on \(\alpha\) are the last \(k\) of the gate values \((v_0, \dots, v_{m-1})\) of \(C\) on \(\alpha\) as a circuit on \(n + 2\) inputs, that is \((v_{m-k}, \dots, v_{m-1})\); when \(k > m\) they are all \(m\) gate values.

def s3CircuitOutputs (C : List S3Gate) (assign : List Bool) (k n : ℕ) : List Bool :=
  let vals := s3CircuitEval C assign n
  vals.drop (vals.length - k)
Uses 2 · Used by 1
Statement usesEncoded gates · Gate values of an encoded circuit
Used byLiterals of a succinctly described formula

DefinitionValid gates of a succinct 3SAT descriptor#✓fully proved

Let \(C\) be a list of gates encoded as (kind, references) pairs and let \(n\) and \(j\) be natural numbers. Gate \(j\) of \(C\) is valid when \(C\) has more than \(j\) entries and its entry \(j\) (counting from \(0\)) is one of: \((0, [i])\) with \(i < n + 2\) (an input gate); \((1, [b])\) with \(b \le 1\) (a constant gate); \((2, [a])\) with \(a < j\) (a negation gate); or \((3, r)\) or \((4, r)\) where every entry \(a\) of \(r\) satisfies \(a < j\) (a conjunction or disjunction gate). Every other entry is invalid.

def s3ValidGate (C : List S3Gate) (n j : ℕ) : Prop :=
  match C[j]? with
  | some (0, [i]) => i < n + 2
  | some (1, [b]) => b ≤ 1
  | some (2, [a]) => a < j
  | some (3, l) => ∀ a ∈ l, a < j
  | some (4, l) => ∀ a ∈ l, a < j
  | _ => False
Uses 1 · Used by 1
Statement usesEncoded gates
Used byWell-formed succinct 3SAT descriptors

DefinitionWell-formed succinct 3SAT descriptors#✓fully proved

Let \(C\) be a list of gates encoded as (kind, references) pairs and let \(n\) be a natural number. The descriptor \(C\) is well-formed for \(n\) when \(C\) has at least \(n + 1\) gates, every gate of \(C\) is valid for \(n\), and the flat Boolean circuit on \(n + 2\) inputs obtained by decoding every gate of \(C\) is well-formed.

def s3WellFormed (C : List S3Gate) (n : ℕ) : Prop :=
  n + 1 ≤ C.length ∧
    (∀ j, j < C.length → s3ValidGate C n j) ∧
    WellFormedCircuit (C.map (acGateOfPair (n := n + 2)))
Uses 5 · Used by 1
Statement usesGates of a flat Boolean circuit · Well-formed flat circuits · Decoding a gate from its (kind, references) pair · Encoded gates · Valid gates of a succinct 3SAT descriptor
Used bySuccinct 3SAT

DefinitionLowest \(n\) bits of a number, least significant first#✓fully proved

For natural numbers \(i\) and \(n\), this is the list of booleans \((b_0, \dots, b_{n-1})\) of length \(n\) in which \(b_k\) is true exactly when \(\lfloor i / 2^k \rfloor\) is odd: the \(n\) lowest binary digits of \(i\), least significant bit first.

def s3BitsOf (i n : ℕ) : List Bool :=
  (List.range n).map (fun k => decide ((i / 2 ^ k) % 2 = 1))
Used by 1
Used byLiterals of a succinctly described formula

DefinitionValue of a list of bits, least significant first#✓fully proved

A list of booleans \((b_0, \dots, b_{m-1})\) represents the natural number \(\sum_{k < m} [b_k]\, 2^k\), where \([b_k]\) is \(1\) if \(b_k\) is true and \(0\) otherwise.

def s3BitsToNum : List Bool → ℕ
  | [] => 0
  | b :: rest => (if b then 1 else 0) + 2 * s3BitsToNum rest
Used by 1
Used byLiterals of a succinctly described formula

DefinitionLiterals of a succinctly described formula#✓fully proved

Let \(C\) be a list of gates encoded as (kind, references) pairs and let \(n\), \(i\) and \(j\) be natural numbers. Give \(C\), as a circuit on \(n + 2\) inputs, the input consisting of the \(n\) lowest bits of \(i\) followed by the \(2\) lowest bits of \(j\), each least significant bit first, and let \((o_0, \dots, o_{p-1})\) be its last \(n + 1\) outputs. Literal \(j\) of clause \(i\) is the pair \((v, s)\) with \(v = \sum_{k < \min(n, p)} [o_k]\, 2^k\), where \([o_k]\) is \(1\) if \(o_k\) is true and \(0\) otherwise, and polarity \(s = o_n\), read as false when \(p \le n\).

def succLiteral (C : List S3Gate) (n i j : ℕ) : ℕ × Bool :=
  let outs := s3CircuitOutputs C (s3BitsOf i n ++ s3BitsOf j 2) (n + 1) n
  (s3BitsToNum (outs.take n), outs.getD n false)
Uses 4 · Used by 1
Statement usesEncoded gates · Lowest \(n\) bits of a number, least significant first · Value of a list of bits, least significant first · Outputs of an encoded circuit
Used bySatisfied clauses of a succinctly described formula

DefinitionSatisfied clauses of a succinctly described formula#✓fully proved

Let \(C\) be a list of gates encoded as (kind, references) pairs, let \(n\) and \(i\) be natural numbers, and let \(\sigma\) assign a boolean to every natural number. Clause \(i\) of the formula described by \(C\) for \(n\) is satisfied by \(\sigma\) when, for some \(j < 3\), literal \(j\) of clause \(i\) of that formula is a pair \((v, s)\) with \(\sigma(v) = s\).

def succClauseSat (C : List S3Gate) (n : ℕ) (assign : ℕ → Bool) (i : ℕ) : Prop :=
  ∃ j, j < 3 ∧
    match succLiteral C n i j with
    | (v, pol) => assign v = pol
Uses 2 · Used by 1
Statement usesEncoded gates · Literals of a succinctly described formula
Used bySuccinct 3SAT

DefinitionSuccinct 3SAT#✓fully proved

Succinct 3SAT is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a pair \((n, C)\) of a natural number \(n\) and a list \(C\) of gates encoded as (kind, references) pairs such that \(C\) is a well-formed descriptor for \(n\) and some assignment \(\sigma\) of booleans to the natural numbers satisfies clause \(c\) of the formula described by \(C\) for every \(c < 2^n\). Bitstrings that do not decode are rejected.

noncomputable def succinctThreeSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List S3Gate) x with
  | some i => decide (s3WellFormed i.2 i.1 ∧ ∃ assign : ℕ → Bool,
      ∀ c, c < 2 ^ i.1 → succClauseSat i.2 i.1 assign c)
  | none => false
Uses 12 · Used by 1
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 · Encoded gates · Well-formed succinct 3SAT descriptors · Satisfied clauses of a succinctly described formula · Decision problems
Used bySuccinct 3SAT is NEXP-complete

TheoremSuccinct 3SAT is NEXP-complete#●ready to prove

The succinct 3SAT decision problem lies in NEXP, and every decision problem in NEXP has a polynomial-time many-one reduction to it.

public theorem_wanted succinct_three_sat_nexp_complete :
    succinctThreeSatDec ∈ NEXP ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ NEXP → Cslib.CookLevin.PolyManyOneRed L succinctThreeSatDec
Sources
  • C. H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994, Theorem 20.3 (succinct 3SAT is NEXP-complete); C. H. Papadimitriou and M. Yannakakis, "A note on succinct representations of graphs", Information and Control 71 (1986), 181-185.
Uses 5
Statement usesThe complexity class NEXP · Polynomial-time many-one reduction · Succinct 3SAT · Complexity classes · Decision problems
10 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.