Circuit satisfiability

DefinitionCertificate position of a wire#✓fully proved

For a wire that refers to one of \(n\) inputs or one of \(g\) gates, its position in \(\{0, \dots, n + g - 1\}\) is \(k\) if it is input \(k\) and \(n + j\) if it is gate \(j\), so the inputs come first and the gates follow.

@[expose] public def toFin {i g : Nat} (wire : Wire i g) : Fin (i + g) :=
  finSumFinEquiv (Wire.equiv i g wire)

Used by 6

Used byBoolean certificate verifier · Completeness of the Boolean certificate verifier · Characterization of accepted certificates · Short accepted certificates exist exactly for satisfiable circuits · Soundness of the Boolean certificate verifier · Cost of the Boolean certificate verifier

DefinitionBoolean certificate verifier#✓fully proved

Let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output, and let \(b = (b_0, \dots, b_{m-1})\) be an array of truth values, read as a value for each wire: input \(k\) at position \(k\) and gate \(j\) at position \(n + j\). The verifier is a computation with a counted cost. It first checks whether \(m = n + s\), at cost \(1\); if not, it returns false. Otherwise, for each gate \(j < s\) in order, it reads the entries of \(b\) at the positions of the argument wires of gate \(j\), at cost \(1\) per argument, and compares the Boolean interpretation of the operation of gate \(j\) on these values with \(b_{n+j}\), at cost \(1\); finally it reads the entry at the position of the output wire, at cost \(1\). It returns true exactly when every comparison succeeds and that output entry is true.

public def verifyBooleanCertificate {i : Nat}
    (c : Circuit booleanSignature i 1) (cert : Array Bool) : TimeM Nat Bool := do
  TimeM.tick 1
  if cert.size = i + c.size then
    let gatesOK ← checkProgram c.program cert
    TimeM.tick 1
    let output := cert.getD (c.outputs 0).toFin.val false
    pure (gatesOK && output)
  else
    pure false

Uses 3 · Used by 6

Statement usesCertificate position of a wire · Boolean interpretation · Boolean signature

Used byCompleteness of the Boolean certificate verifier · Characterization of accepted certificates · Short accepted certificates exist exactly for satisfiable circuits · Soundness of the Boolean certificate verifier · Cost of the Boolean certificate verifier · Linear cost of the Boolean certificate verifier

TheoremCharacterization of accepted certificates#✓fully proved

Let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output, and let \(b = (b_0, \dots, b_{m-1})\) be an array of truth values, where an entry at a position at or beyond \(m\) is read as false and the position of a wire is \(k\) for input \(k\) and \(n + j\) for gate \(j\). The Boolean certificate verifier accepts \(b\) if and only if \(m = n + s\), for every gate \(j < s\) the Boolean interpretation of the operation of gate \(j\) applied to the entries of \(b\) at the positions of its argument wires equals \(b_{n+j}\), and the entry of \(b\) at the position of the output wire is true.

public theorem verifyBooleanCertificate_iff {i : Nat}
    (c : Circuit booleanSignature i 1) (cert : Array Bool) :
    (verifyBooleanCertificate c cert).ret = true ↔
      cert.size = i + c.size ∧
      (∀ j : Fin c.size, booleanInterpretation (c.program.lines j).op
        (fun k => cert.getD ((c.program.lines j).wires k).toFin.val false) =
          cert.getD (i + j.val) false) ∧ cert.getD (c.outputs 0).toFin.val false = true

Uses 4 · Used by 2

Statement usesBoolean certificate verifier · Certificate position of a wire · Boolean interpretation · Boolean signature

Used byCompleteness of the Boolean certificate verifier · Soundness of the Boolean certificate verifier

TheoremSoundness of the Boolean certificate verifier#✓fully proved

Let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output, and let \(b = (b_0, \dots, b_{m-1})\) be an array of truth values, where an entry at a position at or beyond \(m\) is read as false and the position of a wire is \(k\) for input \(k\) and \(n + j\) for gate \(j\). If the Boolean certificate verifier accepts \(b\), then, writing \(x = (b_0, \dots, b_{n-1})\), the value of every wire of \(c\) on input \(x\) under the Boolean interpretation equals the entry of \(b\) at the position of that wire, and the output of \(c\) on input \(x\) is true.

public theorem verifyBooleanCertificate_sound {i : Nat}
    (c : Circuit booleanSignature i 1) (cert : Array Bool)
    (h : (verifyBooleanCertificate c cert).ret = true) :
    (∀ w : Wire i c.size, c.program.trace booleanInterpretation
      (fun k => cert.getD k.val false) w = cert.getD w.toFin.val false) ∧
      c.eval booleanInterpretation (fun k => cert.getD k.val false) 0 = true

Uses 5 · Used by 1

Statement usesBoolean certificate verifier · Certificate position of a wire · Boolean interpretation · Boolean signature

Proof usesCharacterization of accepted certificates

Used byShort accepted certificates exist exactly for satisfiable circuits

TheoremCompleteness of the Boolean certificate verifier#✓fully proved

Let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output, and let \(x = (x_0, \dots, x_{n-1})\) be truth values on which the output of \(c\) under the Boolean interpretation is true. Let \(b\) be the array \((x_0, \dots, x_{n-1}, v_0, \dots, v_{s-1})\), where \(v_j\) is the value of gate \(j\) of \(c\) on input \(x\). Then \(b\) has length \(n + s\) and the Boolean certificate verifier accepts \(b\).

public theorem verifyBooleanCertificate_complete {i : Nat}
    (c : Circuit booleanSignature i 1) (input : Fin i → Bool)
    (h : c.eval booleanInterpretation input 0 = true) :
    let cert := Array.ofFn (Fin.addCases input (c.program.eval booleanInterpretation input))
    cert.size = i + c.size ∧ (verifyBooleanCertificate c cert).ret = true

Uses 5 · Used by 1

Statement usesBoolean certificate verifier · Boolean interpretation · Boolean signature

Proof usesCharacterization of accepted certificates · Certificate position of a wire

Used byShort accepted certificates exist exactly for satisfiable circuits

TheoremShort accepted certificates exist exactly for satisfiable circuits#✓fully proved

Let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output. The Boolean certificate verifier accepts some array of at most \(n + 2s\) truth values if and only if there are truth values \(x_0, \dots, x_{n-1}\) on which the output of \(c\) under the Boolean interpretation is true.

public theorem verifyBooleanCertificate_satisfiable_iff {i : Nat}
    (c : Circuit booleanSignature i 1) :
    (∃ cert : Array Bool, (verifyBooleanCertificate c cert).ret = true ∧
      cert.size ≤ i + 2 * c.size) ↔
      ∃ input : Fin i → Bool, c.eval booleanInterpretation input 0 = true

Uses 6

Statement usesBoolean certificate verifier · Boolean interpretation · Boolean signature

Proof usesCompleteness of the Boolean certificate verifier · Soundness of the Boolean certificate verifier · Certificate position of a wire

TheoremCost of the Boolean certificate verifier#✓fully proved

Let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output, and let \(b\) be an array of \(m\) truth values. The cost counted by the Boolean certificate verifier on \(b\) is \(2 + s + \sum_{j < s} a_j\) if \(m = n + s\), where \(a_j\) is the number of arguments of gate \(j\), and \(1\) otherwise.

public theorem verifyBooleanCertificate_time {i : Nat}
    (c : Circuit booleanSignature i 1) (cert : Array Bool) :
    (verifyBooleanCertificate c cert).time =
      if cert.size = i + c.size then
        2 + c.size + ∑ j : Fin c.size, booleanSignature.Arity (c.program.lines j).op
      else 1

Uses 4 · Used by 1

Statement usesBoolean certificate verifier · Boolean signature

Proof usesCertificate position of a wire · Boolean interpretation

Used byLinear cost of the Boolean certificate verifier

TheoremLinear cost of the Boolean certificate verifier#✓fully proved

Let \(K\) be a natural number and let \(c\) be a circuit over the Boolean signature with \(n\) inputs, \(s\) gates and one output in which every gate has at most \(K\) arguments. Then for every array \(b\) of truth values, the cost counted by the Boolean certificate verifier on \(b\) is at most \(2 + (K + 1)s\).

public theorem verifyBooleanCertificate_time_le_of_fanInAtMost {i K : Nat}
    (c : Circuit booleanSignature i 1) (cert : Array Bool) (hfan : c.FanInAtMost K) :
    (verifyBooleanCertificate c cert).time ≤ 2 + (K + 1) * c.size

Uses 3

Statement usesBoolean certificate verifier · Boolean signature

Proof usesCost of the Boolean certificate verifier

AbbreviationCircuit-satisfiability instances#✓fully proved

An instance of circuit satisfiability is a pair \((n, G)\) of a natural number \(n\), the number of variables, and a finite list \(G\) of gates, each gate a triple \((o, a, b)\) of natural numbers: an operation code \(o\), a first input \(a\) and a second input \(b\).

abbrev CircuitSatInstance := ℕ × List (ℕ × ℕ × ℕ)

Used by 3

Used byThe CIRCUIT SAT decision problem · Satisfiable circuit instances · Well-formed circuit-satisfiability instances

DefinitionResolving a circuit input#✓fully proved

Given an assignment \(x = (x_0, \dots, x_{n-1})\) of booleans to the variables and the list \(v = (v_0, \dots, v_{k-1})\) of the values of the gates evaluated so far, an input index \(r\) resolves to \(x_r\) if \(r < n\), to \(v_{r-n}\) if \(n \le r < n + k\), and to false if \(r \ge n + k\).

def CircuitRef (assign : List Bool) (vals : List Bool) (idx : ℕ) : Bool :=
  if idx < assign.length then assign.getD idx false
  else vals.getD (idx - assign.length) false

Used by 1

Used byValue of a gate

DefinitionValue of a gate#✓fully proved

Let \(x = (x_0, \dots, x_{n-1})\) be an assignment of booleans to the variables and \(v\) the list of values of the earlier gates. An input index \(r\) resolves to \(x_r\) if \(r < n\), and otherwise to \(v_{r-n}\), or to false if that entry does not exist. The value of a gate \((o, a, b)\) is the conjunction of the resolved inputs \(a\) and \(b\) if \(o = 0\), their disjunction if \(o = 1\), the negation of the resolved input \(a\) if \(o = 2\), \(x_a\) (false if \(a \ge n\)) if \(o = 3\), true if \(o = 4\), and false if \(o \ge 5\).

def GateValue (assign : List Bool) (vals : List Bool) (gate : ℕ × ℕ × ℕ) : Bool :=
  match gate.1 with
  | 0 => CircuitRef assign vals gate.2.1 && CircuitRef assign vals gate.2.2
  | 1 => CircuitRef assign vals gate.2.1 || CircuitRef assign vals gate.2.2
  | 2 => !CircuitRef assign vals gate.2.1
  | 3 => assign.getD gate.2.1 false
  | 4 => true
  | _ => false

Uses 1 · Used by 1

Statement usesResolving a circuit input

Used byEvaluating a circuit

DefinitionEvaluating a circuit#✓fully proved

Given an assignment of booleans to the variables and a list of gates \(g_1, \dots, g_m\), circuit evaluation returns the list \((v_1, \dots, v_m)\) of gate values, where \(v_k\) is the value of the gate \(g_k\) under the assignment and the earlier values \((v_1, \dots, v_{k-1})\).

def EvalCircuit (assign : List Bool) (gates : List (ℕ × ℕ × ℕ)) : List Bool :=
  gates.foldl (fun vals gate => vals ++ [GateValue assign vals gate]) []

Uses 1 · Used by 1

Statement usesValue of a gate

Used bySatisfiable circuit instances

DefinitionWell-formed circuit-satisfiability instances#✓fully proved

An instance \((n, G)\) with gates \(G = (g_0, \dots, g_{m-1})\) is well formed when every gate \(g_j = (o, a, b)\) satisfies \(o \le 5\), and moreover: if \(o = 0\) or \(o = 1\) then \(a < n + j\) and \(b < n + j\); if \(o = 2\) then \(a < n + j\); and if \(o = 3\) then \(a < n\).

def WellFormed (i : CircuitSatInstance) : Prop :=
  (∀ p ∈ i.2.zipIdx, p.1.1 ≤ 5 ∧
    ((p.1.1 = 0 ∨ p.1.1 = 1) → p.1.2.1 < i.1 + p.2 ∧ p.1.2.2 < i.1 + p.2) ∧
    (p.1.1 = 2 → p.1.2.1 < i.1 + p.2) ∧
    (p.1.1 = 3 → p.1.2.1 < i.1))

Uses 1 · Used by 1

Statement usesCircuit-satisfiability instances

Used byThe CIRCUIT SAT decision problem

DefinitionSatisfiable circuit instances#✓fully proved

An instance \((n, G)\) is satisfiable when there is an assignment \(x \in \{\mathrm{true}, \mathrm{false}\}^n\) of booleans to the \(n\) variables such that the evaluation of the circuit \(G\) under \(x\) has a last gate value and that value is true. In particular an instance with no gates is not satisfiable.

def CircuitSatFeasible
    (i : CircuitSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    (EvalCircuit assign i.2).getLast? = some true

Uses 2 · Used by 1

Statement usesCircuit-satisfiability instances · Evaluating a circuit

Used byThe CIRCUIT SAT decision problem

DefinitionThe CIRCUIT SAT decision problem#✓fully proved

CIRCUIT SAT is the decision problem that accepts a bitstring \(s\) exactly when \(s\) decodes, under the canonical bitstring encoding of circuit-satisfiability instances, to an instance that is well formed and satisfiable. Bitstrings that fail to decode are rejected.

noncomputable def circuitSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := CircuitSatInstance) x with
  | some i => decide (WellFormed i ∧ CircuitSatFeasible i)
  | 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 · Satisfiable circuit instances · Circuit-satisfiability instances · Well-formed circuit-satisfiability instances · Decision problems

Used byCIRCUIT SAT is NP-complete

TheoremCIRCUIT SAT is NP-complete#●ready to prove

The CIRCUIT SAT decision problem on bitstrings belongs to the class NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

public theorem_wanted circuitSat_npComplete :
    circuitSatDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L circuitSatDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), CIRCUIT SATISFIABILITY; S. A. Cook, "The complexity of theorem-proving procedures" (1971).

Uses 5

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

15 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.