Restricting CNF and DNF formulas

Restriction performs the semantic simplification needed by switching-lemma arguments:

• a satisfied CNF clause or falsified DNF term is removed;
• fixed literals with the neutral value are removed from their clause or term;
• free literals retain their order.

The result preserves evaluation and cannot increase clause/term count or width.

Main results

• CNF.eval_restrict / DNF.eval_restrict -- semantic preservation.
• CNF.complexity_restrict_le / DNF.complexity_restrict_le.
• CNF.width_restrict_le / DNF.width_restrict_le.

def Complexity.Literal.restrictValue {N : ℕ} (ρ : Restriction.On N) (literal : Literal N) : Option Bool

Evaluate a literal when its variable is fixed, or return none when the variable remains free.

Equations

• Complexity.Literal.restrictValue ρ literal = match ρ literal.var with | none => none | some value => some (if literal.polarity = true then value else !value)

theorem Complexity.Literal.restrictValue_eq_none_iff {N : ℕ} (ρ : Restriction.On N) (literal : Literal N) : restrictValue ρ literal = none ↔ ρ literal.var = none

A literal survives restriction exactly when its variable is free.

theorem Complexity.Literal.restrictValue_eq_some_true_iff {N : ℕ} (ρ : Restriction.On N) (literal : Literal N) : restrictValue ρ literal = some true ↔ ρ literal.var = some literal.polarity

A fixed literal evaluates to true exactly when its variable is fixed to the literal's polarity.

theorem Complexity.Literal.restrictValue_eq_some_false_iff {N : ℕ} (ρ : Restriction.On N) (literal : Literal N) : restrictValue ρ literal = some false ↔ ρ literal.var = some !literal.polarity

A fixed literal evaluates to false exactly when its variable is fixed opposite to the literal's polarity.

theorem Complexity.Literal.restrictValue_neg {N : ℕ} (ρ : Restriction.On N) (literal : Literal N) : restrictValue ρ literal.neg = Option.map (fun (x : Bool) => !x) (restrictValue ρ literal)

Restriction turns literal negation into Boolean negation of the fixed value, while leaving a free literal free.

theorem Complexity.Literal.restrictValue_comp {N : ℕ} (first second : Restriction.On N) (literal : Literal N) : restrictValue (first.comp second) literal = (restrictValue first literal).or (restrictValue second literal)

Restricting a literal by a left-biased composite first consults the first restriction and then the second one.

theorem Complexity.Literal.eval_applyTo {N : ℕ} (ρ : Restriction.On N) (x : BitString N) (literal : Literal N) : literal.eval (ρ.applyTo x) = (restrictValue ρ literal).getD (literal.eval x)

A literal evaluated after applying a restriction is either its fixed value or its value on the remaining assignment.

def Complexity.CNF.restrictClause {N : ℕ} (ρ : Restriction.On N) : List (Literal N) → Option (List (Literal N))

Restrict one clause.

none means that a fixed true literal satisfies the clause. some reduced contains the remaining free literals; some [] is an unsatisfied empty clause.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CNF.restrictClause ρ [] = some []

def Complexity.CNF.restrict {N : ℕ} (ρ : Restriction.On N) (φ : CNF N) : CNF N

Simplify a CNF under a finite-arity restriction.

Equations

• Complexity.CNF.restrict ρ φ = { clauses := List.filterMap (Complexity.CNF.restrictClause ρ) φ.clauses }

theorem Complexity.CNF.eval_restrict {N : ℕ} (ρ : Restriction.On N) (x : BitString N) (φ : CNF N) : (restrict ρ φ).eval x = φ.eval (ρ.applyTo x)

Restricting a CNF and then evaluating it agrees with evaluating the original CNF after applying the restriction to its assignment.

theorem Complexity.CNF.complexity_restrict_le {N : ℕ} (ρ : Restriction.On N) (φ : CNF N) : (restrict ρ φ).complexity ≤ φ.complexity

Restriction cannot increase a CNF's number of clauses.

theorem Complexity.CNF.width_restrict_le {N : ℕ} (ρ : Restriction.On N) (φ : CNF N) : (restrict ρ φ).width ≤ φ.width

Restriction cannot increase a CNF's maximum clause width.

theorem Complexity.CNF.vars_restrict_subset_filter {N : ℕ} (ρ : Restriction.On N) (φ : CNF N) : (restrict ρ φ).vars ⊆ {index ∈ φ.vars | ρ index = none}

Every variable surviving CNF simplification occurred originally and is free under the restriction.

def Complexity.DNF.restrictTerm {N : ℕ} (ρ : Restriction.On N) : List (Literal N) → Option (List (Literal N))

Restrict one term.

none means that a fixed false literal falsifies the term. some reduced contains the remaining free literals; some [] is a satisfied empty term.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DNF.restrictTerm ρ [] = some []

theorem Complexity.DNF.restrictTerm_map_neg {N : ℕ} (ρ : Restriction.On N) (clause : List (Literal N)) : restrictTerm ρ (List.map Literal.neg clause) = Option.map (List.map Literal.neg) (CNF.restrictClause ρ clause)

Restricting the negation of a CNF clause agrees with restricting the clause and negating every surviving literal.

def Complexity.DNF.restrict {N : ℕ} (ρ : Restriction.On N) (φ : DNF N) : DNF N

Simplify a DNF under a finite-arity restriction.

Equations

• Complexity.DNF.restrict ρ φ = { terms := List.filterMap (Complexity.DNF.restrictTerm ρ) φ.terms }

theorem Complexity.DNF.exists_restrictTerm_eq_some_iff {N : ℕ} (ρ : Restriction.On N) (term : List (Literal N)) : (∃ (reduced : List (Literal N)), restrictTerm ρ term = some reduced) ↔ ∀ literal ∈ term, ρ literal.var = none ∨ ρ literal.var = some literal.polarity

A DNF term survives exactly when each of its fixed literals is fixed to its satisfying polarity.

theorem Complexity.DNF.restrictTerm_eq_some_filter_iff {N : ℕ} (ρ : Restriction.On N) (term : List (Literal N)) : restrictTerm ρ term = some (List.filter (fun (literal : Literal N) => decide (ρ literal.var = none)) term) ↔ ∀ literal ∈ term, ρ literal.var = none ∨ ρ literal.var = some literal.polarity

When a term survives, its exact reduction is obtained by retaining precisely the literals whose variables remain free.

theorem Complexity.DNF.restrictTerm_comp {N : ℕ} (first second : Restriction.On N) (term : List (Literal N)) : restrictTerm (first.comp second) term = (restrictTerm first term).bind (restrictTerm second)

Successively restricting one term agrees exactly with restricting by the left-biased composite.

theorem Complexity.DNF.restrictTerm_comp_eq_none_of_eq_none {N : ℕ} (first second : Restriction.On N) (term : List (Literal N)) (hkilled : restrictTerm first term = none) : restrictTerm (first.comp second) term = none

Once a term is killed, every extension of the restriction also kills it.

theorem Complexity.DNF.restrict_comp {N : ℕ} (first second : Restriction.On N) (formula : DNF N) : restrict second (restrict first formula) = restrict (first.comp second) formula

Applying two DNF restrictions successively is syntactically identical to applying their left-biased composite once.

theorem Complexity.DNF.eval_restrict {N : ℕ} (ρ : Restriction.On N) (x : BitString N) (φ : DNF N) : (restrict ρ φ).eval x = φ.eval (ρ.applyTo x)

Restricting a DNF and then evaluating it agrees with evaluating the original DNF after applying the restriction to its assignment.

theorem Complexity.DNF.mem_of_mem_restrictTerm {N : ℕ} (ρ : Restriction.On N) {term reduced : List (Literal N)} (hrestrict : restrictTerm ρ term = some reduced) {literal : Literal N} (hmem : literal ∈ reduced) : literal ∈ term ∧ ρ literal.var = none

Every literal retained in a restricted DNF term occurred originally and its variable is free under the restriction.

theorem Complexity.DNF.complexity_restrict_le {N : ℕ} (ρ : Restriction.On N) (φ : DNF N) : (restrict ρ φ).complexity ≤ φ.complexity

Restriction cannot increase a DNF's number of terms.

theorem Complexity.DNF.width_restrict_le {N : ℕ} (ρ : Restriction.On N) (φ : DNF N) : (restrict ρ φ).width ≤ φ.width

Restriction cannot increase a DNF's maximum term width.

theorem Complexity.DNF.vars_restrict_subset_filter {N : ℕ} (ρ : Restriction.On N) (φ : DNF N) : (restrict ρ φ).vars ⊆ {index ∈ φ.vars | ρ index = none}

Every variable surviving DNF simplification occurred originally and is free under the restriction.

theorem Complexity.CNF.restrictClause_map_neg {N : ℕ} (ρ : Restriction.On N) (term : List (Literal N)) : restrictClause ρ (List.map Literal.neg term) = Option.map (List.map Literal.neg) (DNF.restrictTerm ρ term)

Restricting the negation of a DNF term agrees with restricting the term and negating every surviving literal.

theorem Complexity.CNF.neg_restrict {N : ℕ} (ρ : Restriction.On N) (formula : CNF N) : (restrict ρ formula).neg = DNF.restrict ρ formula.neg

Restriction commutes exactly with De Morgan negation from CNF to DNF.

theorem Complexity.DNF.neg_restrict {N : ℕ} (ρ : Restriction.On N) (formula : DNF N) : (restrict ρ formula).neg = CNF.restrict ρ formula.neg

Restriction commutes exactly with De Morgan negation from DNF to CNF.