`CNFFormula`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.RSatEncoding
domain: Complexity
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.RSatEncoding on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  45  size_bound : literals.length ≤ 3
  46
  47/-- A k-CNF formula is a list of clauses over n variables. -/
  48structure CNFFormula (n : ℕ) where
  49  clauses : List (Clause n)
  50  var_count : ℕ
  51  var_count_eq : var_count = n
  52
  53/-- An assignment is a Boolean function on variables. -/
  54def Assignment (n : ℕ) := Fin n → Bool
  55
  56/-- A literal is satisfied by an assignment. -/
  57def Literal.satisfiedBy {n : ℕ} (lit : Fin n × Bool) (a : Assignment n) : Bool :=
  58  if lit.2 then a lit.1 else !a lit.1
  59
  60/-- A clause is satisfied if at least one literal is satisfied. -/
  61def Clause.satisfiedBy {n : ℕ} (c : Clause n) (a : Assignment n) : Bool :=
  62  c.literals.any (fun lit => Literal.satisfiedBy lit a)
  63
  64/-- A CNF formula is satisfied if all clauses are satisfied. -/
  65def CNFFormula.satisfiedBy {n : ℕ} (f : CNFFormula n) (a : Assignment n) : Bool :=
  66  f.clauses.all (fun c => c.satisfiedBy a)
  67
  68/-- A formula is satisfiable if there exists a satisfying assignment. -/
  69def CNFFormula.isSAT {n : ℕ} (f : CNFFormula n) : Prop :=
  70  ∃ a : Assignment n, f.satisfiedBy a = true
  71
  72/-- A formula is UNSAT if no assignment satisfies it. -/
  73def CNFFormula.isUNSAT {n : ℕ} (f : CNFFormula n) : Prop :=
  74  ∀ a : Assignment n, f.satisfiedBy a = false
  75
  76/-! ## J-Cost Landscape for SAT -/
  77
  78/-- The J-cost of a formula under an assignment.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.