Circuit value problem

AbbreviationEncoded circuit gates#✓fully proved

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

Such a pair is read as a gate by the shared (kind, references) decoding of flat circuit gates.

abbrev CVGate := ℕ × List ℕ

Used by 3

Used byEvaluation of an encoded Boolean circuit · The Circuit Value Problem · Well-formed encoded circuits

DefinitionEvaluation of an encoded Boolean circuit#✓fully proved

Let \(n\) be a number of inputs, let \(C\) be a list of gates, each encoded as a (kind, references) pair, and let \(a = (a_0, a_1, \dots)\) be a list of booleans. The evaluation of \(C\) on \(a\) is the list of values of all gates, in order, of the flat Boolean circuit on \(n\) inputs obtained by decoding each pair of \(C\), under the assignment that sends each input \(i < n\) to \(a_i\), or to false when \(i\) is at least the length of \(a\).

def cvCircuitEval {n : ℕ} (C : List CVGate) (assign : List Bool) : List Bool :=
  circuitEval (C.map (acGateOfPair (n := n))) (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 circuit gates

Used byThe Circuit Value Problem

DefinitionWell-formed encoded circuits#✓fully proved

A list \(C\) of encoded gates, each a (kind, references) pair, is well formed as a circuit on \(n\) inputs when the flat Boolean circuit on \(n\) inputs obtained by decoding each pair of \(C\) is well formed: every decoded gate references only strictly earlier gates.

def CVWellFormed {n : ℕ} (C : List CVGate) : Prop :=
  WellFormedCircuit (C.map (acGateOfPair (n := n)))

Uses 4 · Used by 1

Statement usesGates of a flat Boolean circuit · Well-formed flat circuits · Decoding a gate from its (kind, references) pair · Encoded circuit gates

Used byThe Circuit Value Problem

DefinitionThe Circuit Value Problem#✓fully proved

The Circuit Value Problem is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of such triples, to a triple \((n, C, a)\) of a natural number \(n\), a list \(C\) of encoded gates and a list \(a\) of booleans such that the flat Boolean circuit on \(n\) inputs obtained by decoding the gates of \(C\) is well formed, \(a\) has length \(n\), and the evaluation of \(C\) on \(a\) is a nonempty list whose last entry is true. It rejects every bitstring that does not decode.

noncomputable def cvpDec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List CVGate × List Bool) x with
  | some i => decide (CVWellFormed (n := i.1) i.2.1 ∧ i.2.2.length = i.1 ∧
      (cvCircuitEval (n := i.1) i.2.1 i.2.2).getLast? = some true)
  | 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 circuit gates · Well-formed encoded circuits · Evaluation of an encoded Boolean circuit · Decision problems

Used byThe Circuit Value Problem is P-complete

TheoremThe Circuit Value Problem is P-complete#●ready to prove

The Circuit Value Problem is in P, and every decision problem in P is log-space many-one reducible to the Circuit Value Problem.

public theorem_wanted cvp_p_complete :
    cvpDec ∈ MetaMathlibExt.ComplexityTheory.P ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.P → LogSpaceRed L cvpDec

Sources

• R. E. Ladner, "The circuit value problem is log space complete for P", SIGACT News 7 (1975), 18-20; S. A. Cook, "A hierarchy for nondeterministic time complexity", Journal of Computer and System Sciences 7 (1973), 343-353.

Uses 5

Statement usesLog-space many-one reductions · The Circuit Value Problem · Complexity classes · Decision problems · The complexity class P

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.