`Assignment`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.RSatEncoding on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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.
  79    J = 0 iff all clauses are satisfied (zero defect = satisfying assignment).
  80    J = (number of unsatisfied clauses) > 0 iff UNSAT under this assignment. -/
  81noncomputable def satJCost {n : ℕ} (f : CNFFormula n) (a : Assignment n) : ℝ :=
  82  (f.clauses.filter (fun c => !c.satisfiedBy a)).length
  83
  84/-- J-cost is nonneg (number of unsatisfied clauses ≥ 0). -/

papers checked against this theorem

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