Operations on CNF and DNF

Disjunction of DNFs and conjunction of CNFs preserve the largest component width and add component counts. These operations let a layer of bounded-depth decision trees be assembled into the matching normal form without a distributive expansion.

theorem Complexity.DNF.eval_disjoin {N : ℕ} (formulas : List (DNF N)) (input : BitString N) : (disjoin formulas).eval input = formulas.any fun (formula : DNF N) => formula.eval input

Disjoining DNFs agrees with disjoining their Boolean values.

theorem Complexity.DNF.width_disjoin_le {N : ℕ} (formulas : List (DNF N)) (bound : ℕ) (hbound : ∀ formula ∈ formulas, formula.width ≤ bound) : (disjoin formulas).width ≤ bound

Disjoining DNFs cannot exceed a common width bound.

theorem Complexity.DNF.complexity_disjoin {N : ℕ} (formulas : List (DNF N)) : (disjoin formulas).complexity = (List.map complexity formulas).sum

DNF disjunction adds the numbers of terms exactly.

theorem Complexity.CNF.eval_conjoin {N : ℕ} (formulas : List (CNF N)) (input : BitString N) : (conjoin formulas).eval input = formulas.all fun (formula : CNF N) => formula.eval input

Conjoining CNFs agrees with conjoining their Boolean values.

theorem Complexity.CNF.width_conjoin_le {N : ℕ} (formulas : List (CNF N)) (bound : ℕ) (hbound : ∀ formula ∈ formulas, formula.width ≤ bound) : (conjoin formulas).width ≤ bound

Conjoining CNFs cannot exceed a common width bound.

theorem Complexity.CNF.complexity_conjoin {N : ℕ} (formulas : List (CNF N)) : (conjoin formulas).complexity = (List.map complexity formulas).sum

CNF conjunction adds the numbers of clauses exactly.