Negation normal form of De Morgan formulas

Pushing the negations of a De Morgan formula to the inputs by De Morgan's laws, cancelling double negations and evaluating negated constants, gives a formula in negation normal form (Formula.nnf), with negations only directly on inputs (Formula.IsNNF, Formula.isNNF_nnf). It computes the same function (Formula.eval_nnf) with the same leaves (Formula.leafSize_nnf) Jukna, Chapter 6. Its depth counts every gate, negations included, and is at most one more than the number of AND and OR gates on a path of the original formula (Formula.depth_nnf_le). So the depth of a function with negations and constants free, Boolean.formulaDepth, and its depth with every gate counted differ by at most one (Formula.depthWith_le_depth, Boolean.exists_computes_depth_le_formulaDepth_add_one).

Main definitions

• Cslib.Circuits.Formula.IsNNF: formulas whose negations apply directly to inputs.
• Cslib.Circuits.Formula.nnf: the negation normal form of a De Morgan formula or of its negation.

Main results

• Cslib.Circuits.Formula.isNNF_nnf: the negation normal form is in negation normal form.
• Cslib.Circuits.Formula.eval_nnf, Cslib.Circuits.Formula.leafSize_nnf: the negation normal form computes the same function with the same leaves.
• Cslib.Circuits.Formula.depth_nnf_le: its depth is at most one more than the depth with negations and constants free.
• Cslib.Circuits.Boolean.exists_computes_depth_le_formulaDepth_add_one: every function has a formula whose depth exceeds its formula depth by at most one.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

def Cslib.Circuits.Formula.nnf {n : ℕ} : Formula Boolean.signature n → Bool → Formula Boolean.signature n

The negation normal form of a De Morgan formula, of its negation when b is true: negations are pushed to the inputs by De Morgan's laws, double negations cancel, and negated constants are evaluated.

inductive Cslib.Circuits.Formula.IsNNF {n : ℕ} : Formula Boolean.signature n → Prop

A De Morgan formula is in negation normal form when its negations apply directly to inputs: it is built from inputs, negated inputs and constants by conjunctions and disjunctions.

• input {n : ℕ} (i : Fin n) : (Formula.input i).IsNNF

  An input.

• not_input {n : ℕ} (i : Fin n) : (Formula.input i).not.IsNNF

  A negated input.

• const {n : ℕ} (b : Bool) : (Formula.const b).IsNNF

  A constant.

• and {n : ℕ} {F G : Formula Boolean.signature n} : F.IsNNF → G.IsNNF → (F.and G).IsNNF

  A conjunction of formulas in negation normal form.

• or {n : ℕ} {F G : Formula Boolean.signature n} : F.IsNNF → G.IsNNF → (F.or G).IsNNF

  A disjunction of formulas in negation normal form.

theorem Cslib.Circuits.Formula.IsNNF.orList {n : ℕ} {l : List (Formula Boolean.signature n)} (hl : ∀ F ∈ l, F.IsNNF) : (Formula.orList l).IsNNF

A balanced disjunction of formulas in negation normal form is in negation normal form.

theorem Cslib.Circuits.Formula.IsNNF.andList {n : ℕ} {l : List (Formula Boolean.signature n)} (hl : ∀ F ∈ l, F.IsNNF) : (Formula.andList l).IsNNF

A balanced conjunction of formulas in negation normal form is in negation normal form.

theorem Cslib.Circuits.Formula.isNNF_nnf {n : ℕ} (F : Formula Boolean.signature n) (b : Bool) : (F.nnf b).IsNNF

The negation normal form is in negation normal form.

@[simp]

theorem Cslib.Circuits.Formula.eval_nnf {n : ℕ} (F : Formula Boolean.signature n) (b : Bool) (x : BitString n) : (F.nnf b).eval Boolean.interpretation x = (F.eval Boolean.interpretation x ^^ b)

The negation normal form computes the formula, negated when b is true.

@[simp]

theorem Cslib.Circuits.Formula.leafSize_nnf {n : ℕ} (F : Formula Boolean.signature n) (b : Bool) : (F.nnf b).leafSize = F.leafSize

The negation normal form has the leaves of the formula.

theorem Cslib.Circuits.Formula.depth_nnf_le {n : ℕ} (F : Formula Boolean.signature n) (b : Bool) : (F.nnf b).depth ≤ depthWith Boolean.binaryCost F + 1

The negation normal form is deeper than the formula with negations and constants free by at most one.

theorem Cslib.Circuits.Boolean.exists_computes_depth_le_formulaDepth_add_one {n : ℕ} (f : BooleanFunction n) : ∃ (F : Formula signature n), F.Computes interpretation f ∧ F.depth ≤ formulaDepth f + 1

Every Boolean function has a De Morgan formula whose depth, counting every gate, is at most its formula depth plus one.