Unfolding fan-in-two circuit outputs into Boolean formulas -- definitions

These definitions recursively unfold the DAG below one selected circuit wire or output gate. Shared subcircuits are intentionally duplicated in the resulting formula tree; no formula-size claim is implicit in this bridge.

def Complexity.BoolFormula.negateIf (negated : Bool) (formula : BoolFormula) : BoolFormula

Negate a formula exactly when the Boolean edge flag is set.

Equations

• Complexity.BoolFormula.negateIf negated formula = if negated = true then formula.neg else formula

def Complexity.Gate.toBoolFormula {W : ℕ} (gate : Gate Basis.andOr2 W) (wireFormula : Fin W → BoolFormula) : BoolFormula

Replace the two inputs of a fan-in-two AND/OR gate by formulas, retaining the gate operation and its two edge-negation flags.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Complexity.Circuit.wireFormula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (wire : Fin (N + G)) : BoolFormula

Recursively unfold the fan-in-two circuit DAG below wire wire into a Boolean formula over the primary-input indices.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Circuit.outputFormula {N M G : ℕ} [NeZero N] [NeZero M] (circuit : Circuit Basis.andOr2 N M G) (output : Fin M) : BoolFormula

Unfold one selected output gate into a Boolean formula.

Equations

• circuit.outputFormula output = (circuit.outputs output).toBoolFormula fun (wire : Fin (N + G)) => circuit.wireFormula wire