Model-count-preserving CNF transformations

DefinitionModel count of a CNF formula#✓fully proved

The number of Boolean assignments to the variables occurring in a formula that satisfy it.

def modelCount (formula : CNF) : Nat :=
  letI (assignment : {x // x ∈ formula.vars} → Bool) : Decidable
      (formula.Satisfies fun x => if h : x ∈ formula.vars then assignment ⟨x, h⟩ else false) := by
    unfold Satisfies CNFClause.Satisfies CNFLiteral.Satisfies
    infer_instance
  (Finset.univ.filter fun assignment : {x // x ∈ formula.vars} → Bool =>
    formula.Satisfies fun x => if h : x ∈ formula.vars then assignment ⟨x, h⟩ else false).card

Uses 6 · Used by 3

Statement usesCNF formula · Satisfaction of a CNF formula · Variables of a CNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal

Used byCounting satisfying assignments over a larger variable range · Variable compaction preserves the model count · The parsimonious 3-CNF reduction preserves the model count

DefinitionExact variable compaction of a CNF formula#✓fully proved

Rename every occurring variable by its position in the last-occurrence list.

def compact (formula : CNF) : CNF :=
  let names := (formula.flatMap fun clause => clause.map Prod.fst).dedup
  formula.map fun clause => clause.map fun literal => (names.idxOf literal.1, literal.2)

Uses 2 · Used by 7

Statement usesCNF formula · CNF clause

Used byCompaction preserves clause-length bounds · Compaction preserves clause lengths · Compaction preserves the number of clauses · Variable compaction preserves the model count · Compaction preserves absence of duplicate clauses · Satisfaction is preserved by variable compaction · Variables of a compacted formula form an initial range

TheoremCompaction preserves the number of clauses#✓fully proved

Compaction preserves the number of clauses.

@[simp]
theorem length_compact (formula : CNF) : formula.compact.length = formula.length

Uses 3

Statement usesCNF formula · Exact variable compaction of a CNF formula · CNF clause

TheoremCompaction preserves clause lengths#✓fully proved

Compaction preserves every clause length, in the original clause order.

theorem clauseLengths_compact (formula : CNF) :
    formula.compact.map List.length = formula.map List.length

Uses 3

Statement usesCNF formula · Exact variable compaction of a CNF formula

Proof usesCNF clause

TheoremCompaction preserves clause-length bounds#✓fully proved

Compaction preserves every upper bound on clause length.

theorem boundedClauseLength_compact_iff (formula : CNF) (k : Nat) :
    (∀ clause ∈ formula.compact, clause.length ≤ k) ↔
      ∀ clause ∈ formula, clause.length ≤ k

Uses 3

Statement usesCNF formula · Exact variable compaction of a CNF formula · CNF clause

TheoremCompaction preserves absence of duplicate clauses#✓fully proved

Compaction preserves the absence of duplicate clauses.

theorem nodup_compact_iff (formula : CNF) :
    formula.compact.Nodup ↔ formula.Nodup

Uses 5

Statement usesCNF formula · Exact variable compaction of a CNF formula · CNF clause

Proof usesVariables of a CNF formula · Variables of a clause

TheoremVariables of a compacted formula form an initial range#✓fully proved

The variables of a compacted formula are exactly its dense initial range.

theorem vars_compact (formula : CNF) :
    formula.compact.vars = Finset.range formula.vars.card

Uses 5 · Used by 1

Statement usesCNF formula · Exact variable compaction of a CNF formula · Variables of a CNF formula

Proof usesCNF clause · Variables of a clause

Used byVariable compaction preserves the model count

TheoremSatisfaction is preserved by variable compaction#✓fully proved

Satisfaction after compaction is satisfaction before compaction with names translated by their exact last-occurrence positions.

theorem satisfies_compact_iff (formula : CNF) (assignment : Nat → Bool) :
    formula.compact.Satisfies assignment ↔
      formula.Satisfies fun x =>
        assignment ((formula.flatMap fun C => C.map Prod.fst).dedup.idxOf x)

Uses 6 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · Exact variable compaction of a CNF formula · CNF clause

Proof usesSatisfaction of a clause · Satisfaction of a literal

Used byVariable compaction preserves the model count

TheoremVariable compaction preserves the model count#✓fully proved

Exact variable compaction preserves the number of assignments to the occurring variables.

theorem modelCount_compact (formula : CNF) :
    formula.compact.modelCount = formula.modelCount

Uses 11

Statement usesCNF formula · Exact variable compaction of a CNF formula · Model count of a CNF formula

Proof usesSatisfaction of a CNF formula · Satisfaction is preserved by variable compaction · Variables of a CNF formula · Variables of a compacted formula form an initial range · CNF clause · Satisfaction of a clause · Variables of a clause · Satisfaction of a literal

TheoremCounting satisfying assignments over a larger variable range#✓fully proved

If every occurring name is below N, the count over all Fin N assignments is the support count times one Boolean choice for each unused ambient variable.

theorem card_satisfying_fin (formula : CNF) (N : Nat)
    (hvars : ∀ x ∈ formula.vars, x < N) :
    Nat.card {assignment : Fin N → Bool //
      formula.Satisfies fun x => if h : x < N then assignment ⟨x, h⟩ else false} =
      2 ^ (N - formula.vars.card) * formula.modelCount

Uses 9

Statement usesCNF formula · Satisfaction of a CNF formula · Model count of a CNF formula · Variables of a CNF formula

Proof usesSatisfaction depends only on the occurring variables · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Number of functions agreeing with a given one on a set

DefinitionNumber of fresh variables in the parsimonious 3-CNF reduction#✓fully proved

The number of fresh variables used by the parsimonious width-three reduction.

def numFreshParsimonious3 (formula : CNF) : Nat :=
  (formula.map fun clause => clause.length - 3).sum

Uses 2 · Used by 6

Statement usesCNF formula · CNF clause

Used byUnique satisfying extension in the parsimonious 3-CNF reduction · The parsimonious reduction outputs a duplicate-free 3-CNF · The parsimonious 3-CNF reduction preserves the model count · Soundness of the parsimonious 3-CNF reduction · Size bounds for the parsimonious 3-CNF reduction · Parsimonious reduction of CNF to 3-CNF

DefinitionParsimonious reduction of CNF to 3-CNF#✓fully proved

Reduce a CNF to clauses of length at most three, allocating fresh variables consecutively from start. Repeated output clauses are removed in last-occurrence order.

Cslib.Logic.PL.CNF.to3Parsimonious · 23 lines

def to3Parsimonious (formula : CNF) (start : Nat) : CNF :=
  (splitAll ((List.range formula.numFreshParsimonious3).map fun offset => start + offset)
    formula).dedup
where
  /-- Negate one literal while preserving its variable name. -/
  neg (literal : Nat × Bool) : Nat × Bool := (literal.1, !literal.2)
  /-- Force `fresh` to equal the disjunction of the first two literals. -/
  forced (fresh : Nat) (first second : Nat × Bool) : CNF :=
    [[(fresh, false), first, second],
      [(fresh, true), neg first],
      [(fresh, true), neg second]]
  /-- Split one clause using its assigned fresh-variable names. -/
  splitClause : List Nat → CNFClause → CNF
    | fresh :: rest, first :: second :: third :: fourth :: tail =>
        forced fresh first second ++
          splitClause rest ((fresh, true) :: third :: fourth :: tail)
    | _, clause => [clause]
  /-- Split every clause, consuming consecutive fresh-variable names. -/
  splitAll : List Nat → CNF → CNF
    | _, [] => []
    | fresh, clause :: rest =>
        splitClause (fresh.take (clause.length - 3)) clause ++
          splitAll (fresh.drop (clause.length - 3)) rest

Uses 3 · Used by 5

Statement usesCNF formula · Number of fresh variables in the parsimonious 3-CNF reduction · CNF clause

Used byUnique satisfying extension in the parsimonious 3-CNF reduction · The parsimonious reduction outputs a duplicate-free 3-CNF · The parsimonious 3-CNF reduction preserves the model count · Soundness of the parsimonious 3-CNF reduction · Size bounds for the parsimonious 3-CNF reduction

TheoremSoundness of the parsimonious 3-CNF reduction#✓fully proved

Satisfaction of the reduced formula implies satisfaction of the original formula under the same values of the original variable names.

theorem satisfies_of_satisfies_to3Parsimonious {formula : CNF} {start : Nat}
    {assignment : Nat → Bool}
    (hsatisfies : (formula.to3Parsimonious start).Satisfies assignment) :
    formula.Satisfies assignment

Uses 7 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · Parsimonious reduction of CNF to 3-CNF

Proof usesNumber of fresh variables in the parsimonious 3-CNF reduction · CNF clause · Satisfaction of a clause · Satisfaction of a literal

Used byThe parsimonious 3-CNF reduction preserves the model count

TheoremThe parsimonious reduction outputs a duplicate-free 3-CNF#✓fully proved

Every output clause has length at most three, and duplicate clauses have been removed.

theorem isThreeCNF_to3Parsimonious (formula : CNF) (start : Nat) :
    (∀ clause ∈ formula.to3Parsimonious start, clause.length ≤ 3) ∧
      (formula.to3Parsimonious start).Nodup

Uses 4

Statement usesCNF formula · Parsimonious reduction of CNF to 3-CNF · CNF clause

Proof usesNumber of fresh variables in the parsimonious 3-CNF reduction

TheoremSize bounds for the parsimonious 3-CNF reduction#✓fully proved

A width bound on the input gives the source bounds on allocated fresh variables and output clauses.

theorem size_to3Parsimonious (formula : CNF) (start k : Nat)
    (hbound : ∀ clause ∈ formula, clause.length ≤ k) :
    formula.numFreshParsimonious3 ≤ (k - 3) * formula.length ∧
      (formula.to3Parsimonious start).length ≤
        formula.length + 3 * ((k - 3) * formula.length)

Uses 4

Statement usesCNF formula · Number of fresh variables in the parsimonious 3-CNF reduction · Parsimonious reduction of CNF to 3-CNF · CNF clause

TheoremUnique satisfying extension in the parsimonious 3-CNF reduction#✓fully proved

Every satisfying assignment of the original formula has exactly one satisfying extension that can differ only on the allocated fresh-variable interval.

theorem existsUnique_satisfies_to3Parsimonious {formula : CNF} {start : Nat}
    {assignment : Nat → Bool}
    (hstart : ∀ x ∈ formula.vars, x < start)
    (hsatisfies : formula.Satisfies assignment) :
    ∃! extension : Nat → Bool,
      (formula.to3Parsimonious start).Satisfies extension ∧
        ∀ x, x < start ∨ start + formula.numFreshParsimonious3 ≤ x →
          extension x = assignment x

Uses 9 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · Number of fresh variables in the parsimonious 3-CNF reduction · Parsimonious reduction of CNF to 3-CNF · Variables of a CNF formula

Proof usesCNF clause · Satisfaction of a clause · Variables of a clause · Satisfaction of a literal

Used byThe parsimonious 3-CNF reduction preserves the model count

TheoremThe parsimonious 3-CNF reduction preserves the model count#✓fully proved

The parsimonious reduction preserves the number of assignments to the variables occurring in the formula.

theorem modelCount_to3Parsimonious (formula : CNF) (start : Nat)
    (hstart : ∀ x ∈ formula.vars, x < start) :
    (formula.to3Parsimonious start).modelCount = formula.modelCount

Uses 13

Statement usesCNF formula · Model count of a CNF formula · Parsimonious reduction of CNF to 3-CNF · Variables of a CNF formula

Proof usesSatisfaction of a CNF formula · Unique satisfying extension in the parsimonious 3-CNF reduction · Number of fresh variables in the parsimonious 3-CNF reduction · Satisfaction depends only on the occurring variables · Soundness of the parsimonious 3-CNF reduction · CNF clause · Satisfaction of a clause · Variables of a clause · Satisfaction of a literal

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.