`Clause`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.RSatEncoding
domain: Complexity
line: 41 · 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 41.

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

  38
  39/-- A k-CNF clause is a list of at most k literal indices (positive = variable index,
  40    negative = negated variable index). We use a simplified 3-SAT encoding. -/
  41structure Clause (n : ℕ) where
  42  /-- Up to 3 literal indices in {1,..,n} with signs -/
  43  literals : List (Fin n × Bool)
  44  /-- At most 3 literals per clause -/
  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

papers checked against this theorem

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