Guessing inputs

Guessing the last p inputs of a Boolean function f of n + p variables gives the function x ↦ ∃ r, f (x ++ r) of n variables (existsGuess), the function computed by a nondeterministic circuit, and dually x ↦ ∀ r, f (x ++ r) (forallGuess). Trying all 2 ^ p guesses side by side and combining the answers with one big disjunction or conjunction computes them with 2 ^ p (C + 3) + 1 gates, where C is the circuit complexity of f (complexity_existsGuess_le, complexity_forallGuess_le).

Main definitions

• Cslib.Circuits.Boolean.existsGuess, Cslib.Circuits.Boolean.forallGuess.

Main results

• Cslib.Circuits.Boolean.complexity_existsGuess_le, Cslib.Circuits.Boolean.complexity_forallGuess_le: guessing p bits multiplies the circuit complexity by at most 2 ^ p, up to an additive constant per guess.

def Cslib.Circuits.Boolean.existsGuess {n p : ℕ} (f : BooleanFunction (n + p)) : BooleanFunction n

Guessing the last p inputs: whether some setting of them makes f true.

def Cslib.Circuits.Boolean.forallGuess {n p : ℕ} (f : BooleanFunction (n + p)) : BooleanFunction n

Guessing the last p inputs universally: whether every setting of them makes f true.

theorem Cslib.Circuits.Boolean.complexity_existsGuess_le {n p : ℕ} (f : BooleanFunction (n + p)) : complexity interpretation (single (existsGuess f)) ≤ 2 ^ p * (complexity interpretation (single f) + 3) + 1

Guessing p bits costs at most 2 ^ p (C + 3) + 1 gates for a function of circuit complexity C.

theorem Cslib.Circuits.Boolean.complexity_forallGuess_le {n p : ℕ} (f : BooleanFunction (n + p)) : complexity interpretation (single (forallGuess f)) ≤ 2 ^ p * (complexity interpretation (single f) + 3) + 1

Guessing p bits universally costs at most 2 ^ p (C + 3) + 1 gates for a function of circuit complexity C.