`Constraint`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.PC
domain: Complexity
line: 10 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.PC on GitHub at line 10.

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

   7namespace SAT
   8
   9/-- Constraints are either CNF-clauses or XOR-checks. -/
  10inductive Constraint (n : Nat) where
  11  | cnf (C : Clause n)
  12  | xor (X : XORConstraint n)
  13deriving Repr
  14
  15/-- Whether a variable is mentioned in a literal. -/
  16def mentionsVarLit {n} (l : Lit n) (v : Var n) : Bool :=
  17  match l with
  18  | .pos u => decide (u = v)
  19  | .neg u => decide (u = v)
  20
  21/-- Whether a variable is mentioned in a clause. -/
  22def mentionsVarClause {n} (C : Clause n) (v : Var n) : Bool :=
  23  C.any (fun l => mentionsVarLit l v)
  24
  25/-- Whether a variable is mentioned in an XOR constraint. -/
  26def mentionsVarXOR {n} (X : XORConstraint n) (v : Var n) : Bool :=
  27  X.vars.any (fun u => decide (u = v))
  28
  29/-- Whether a variable is mentioned in a mixed constraint. -/
  30def mentionsVar {n} (K : Constraint n) (v : Var n) : Bool :=
  31  match K with
  32  | .cnf C => mentionsVarClause C v
  33  | .xor X => mentionsVarXOR X v
  34
  35/-- Satisfaction semantics for mixed constraints. -/
  36def satisfiesConstraint {n} (a : Assignment n) (K : Constraint n) : Prop :=
  37  match K with
  38  | .cnf C => evalClause a C = true
  39  | .xor X => parityOf a X.vars = X.parity
  40

papers checked against this theorem

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