3-CNF formulas

The 3-CNF refinement of the existing CNF type: a CNF is in 3-CNF when every clause has exactly three literals. Following the roadmap (track N3), 3-CNF is introduced here as a predicate on the existing CNF = List Clause, so that all of the CNF semantics (CNF.eval, CNF.Satisfiable, CNF.maxVar, renaming) apply unchanged and a 3-CNF is literally a CNF.

Main definitions and results

• CNF.Is3CNF — every clause has length 3; decidable
• CNF.is3CNF_cons — the cons characterization
• CNF.Is3CNF.mapVar — variable renaming preserves the 3-CNF shape

The substantive N3 milestone — a size-controlled clause-padding transformation turning an arbitrary CNF into an equisatisfiable 3-CNF — builds on this predicate and is tracked separately.

def Complexity.SAT.CNF.Is3CNF (φ : CNF) : Prop

A CNF is in 3-CNF when every clause is a disjunction of exactly three literals. This is a predicate on the existing CNF type, so a 3-CNF formula is literally a CNF and inherits all of its semantics.

Equations

• φ.Is3CNF = ∀ c ∈ φ, List.length c = 3

@[implicit_reducible]

instance Complexity.SAT.instDecidableIs3CNF (φ : CNF) : Decidable φ.Is3CNF

Equations

• Complexity.SAT.instDecidableIs3CNF φ = List.decidableBAll (fun (c : Complexity.SAT.Clause) => List.length c = 3) φ

@[simp]

theorem Complexity.SAT.CNF.is3CNF_nil : Is3CNF []

The empty CNF is trivially in 3-CNF.

@[simp]

theorem Complexity.SAT.CNF.is3CNF_cons {c : Clause} {φ : CNF} : Is3CNF (c :: φ) ↔ List.length c = 3 ∧ φ.Is3CNF

c :: φ is 3-CNF iff c has three literals and φ is 3-CNF.

theorem Complexity.SAT.CNF.Is3CNF.mapVar {φ : CNF} (h : φ.Is3CNF) (f : ℕ → ℕ) : (CNF.mapVar f φ).Is3CNF

Variable renaming preserves the 3-CNF shape: Clause.mapVar maps literals one-for-one, so it does not change clause lengths.

Padding short clauses to width three

A clause with one or two literals is padded to exactly three literals by repeating its last literal. This changes neither the clause's models nor its satisfiability (repeating a literal in a disjunction is idempotent), and turns a CNF whose clauses all have width 1 … 3 into an equivalent 3-CNF. Splitting wide clauses (width > 3) needs fresh Tseitin variables and is tracked separately.

def Complexity.SAT.Clause.padTo3 : Clause → Clause

Pad a clause of one or two literals to width three by repeating a literal; clauses of any other width are left unchanged.

Equations

• Complexity.SAT.Clause.padTo3 [a] = [a, a, a]
• Complexity.SAT.Clause.padTo3 [a, b] = [a, b, b]
• x✝.padTo3 = x✝

theorem Complexity.SAT.Clause.padTo3_eval (α : Assignment) (c : Clause) : eval α c.padTo3 = eval α c

Padding preserves the clause's value under every assignment (repeating a literal in a disjunction is idempotent).

theorem Complexity.SAT.Clause.padTo3_length {c : Clause} (h1 : 1 ≤ List.length c) (h2 : List.length c ≤ 3) : List.length c.padTo3 = 3

A clause of width 1 … 3 is padded to width exactly three.

def Complexity.SAT.CNF.padTo3 (φ : CNF) : CNF

Pad every clause of a CNF to width three.

Equations

• φ.padTo3 = List.map Complexity.SAT.Clause.padTo3 φ

theorem Complexity.SAT.CNF.padTo3_eval (α : Assignment) (φ : CNF) : eval α φ.padTo3 = eval α φ

Padding preserves the CNF's value under every assignment — hence satisfiability.

theorem Complexity.SAT.CNF.padTo3_satisfiable_iff (φ : CNF) : φ.padTo3.Satisfiable ↔ φ.Satisfiable

Padding preserves satisfiability.

theorem Complexity.SAT.CNF.is3CNF_padTo3 {φ : CNF} (h : ∀ c ∈ φ, 1 ≤ List.length c ∧ List.length c ≤ 3) : φ.padTo3.Is3CNF

If every clause of φ has width 1 … 3, then CNF.padTo3 φ is a genuine 3-CNF equivalent to φ.