The semantics of Clause and CNF: evaluation with respect to an assignment, together with the Sat and Unsat predicates built on top of it.

def Std.Sat.CNF.Clause.eval {α : Type u_1} (a : α → Bool) (c : Clause α) : Bool

Evaluating a Clause with respect to an assignment a.

Equations

• Std.Sat.CNF.Clause.eval a c = c.literals.any fun (x : Std.Sat.Literal α) => match x with | (i, n) => a i == n

@[simp]

theorem Std.Sat.CNF.Clause.eval_empty {α : Type u_1} (a : α → Bool) : eval a empty = false

@[simp]

theorem Std.Sat.CNF.Clause.eval_add {α : Type u_1} {atom : α} {pol : Bool} {c : Clause α} (a : α → Bool) : eval a (c.add atom pol) = (a atom == pol || eval a c)

@[simp]

theorem Std.Sat.CNF.Clause.eval_append {α : Type u_1} (a : α → Bool) {c1 c2 : Clause α} : eval a (c1 ++ c2) = (eval a c1 || eval a c2)

theorem Std.Sat.CNF.Clause.eval_congr {α : Type u_1} (a1 a2 : α → Bool) (c : Clause α) (hw : ∀ (i : α), VarMem i c → a1 i = a2 i) : eval a1 c = eval a2 c

def Std.Sat.CNF.Clause.Sat {α : Type u_1} (a : α → Bool) (c : Clause α) : Prop

Equations

• Std.Sat.CNF.Clause.Sat a c = (Std.Sat.CNF.Clause.eval a c = true)

def Std.Sat.CNF.Clause.Unsat {α : Type u_1} (c : Clause α) : Prop

Equations

• c.Unsat = ∀ (a : α → Bool), Std.Sat.CNF.Clause.eval a c = false

theorem Std.Sat.CNF.Clause.sat_def {α : Type u_1} (a : α → Bool) (c : Clause α) : Sat a c ↔ eval a c = true

theorem Std.Sat.CNF.Clause.unsat_def {α : Type u_1} (c : Clause α) : c.Unsat ↔ ∀ (a : α → Bool), eval a c = false

@[simp]

theorem Std.Sat.CNF.Clause.unsat_empty {α : Type u_1} : empty.Unsat

@[simp]

theorem Std.Sat.CNF.Clause.not_sat_empty {α : Type u_1} {a : α → Bool} : ¬Sat a empty

@[simp]

theorem Std.Sat.CNF.Clause.sat_add {α : Type u_1} {atom : α} {pol : Bool} {a : α → Bool} {c : Clause α} : Sat a (c.add atom pol) ↔ a atom = pol ∨ Sat a c

@[simp]

theorem Std.Sat.CNF.Clause.sat_append {α : Type u_1} {a : α → Bool} {c1 c2 : Clause α} : Sat a (c1 ++ c2) ↔ Sat a c1 ∨ Sat a c2

theorem Std.Sat.CNF.Clause.sat_append_left {α : Type u_1} {a : α → Bool} {c1 c2 : Clause α} (h : Sat a c1) : Sat a (c1 ++ c2)

theorem Std.Sat.CNF.Clause.sat_append_right {α : Type u_1} {a : α → Bool} {c1 c2 : Clause α} (h : Sat a c2) : Sat a (c1 ++ c2)

@[simp]

theorem Std.Sat.CNF.Clause.unsat_append {α : Type u_1} {c1 c2 : Clause α} : (c1 ++ c2).Unsat ↔ c1.Unsat ∧ c2.Unsat

theorem Std.Sat.CNF.Clause.unsat_of_unsat_append_left {α : Type u_1} {c1 c2 : Clause α} (h : (c1 ++ c2).Unsat) : c1.Unsat

theorem Std.Sat.CNF.Clause.unsat_of_unsat_append_right {α : Type u_1} {c1 c2 : Clause α} (h : (c1 ++ c2).Unsat) : c2.Unsat

theorem Std.Sat.CNF.Clause.unsat_iff_not_sat {α : Type u_1} {c : Clause α} : c.Unsat ↔ ∀ (a : α → Bool), ¬Sat a c

theorem Std.Sat.CNF.Clause.sat_iff_exists_mem_eq {α : Type u_1} {a : α → Bool} {c : Clause α} : Sat a c ↔ ∃ (lit : Literal α), lit ∈ c ∧ a lit.fst = lit.snd

theorem Std.Sat.CNF.Clause.sat_of_mem_of_eq {α : Type u_1} {a : α → Bool} {c : Clause α} {lit : Literal α} (h1 : lit ∈ c) (h2 : a lit.fst = lit.snd) : Sat a c

theorem Std.Sat.CNF.Clause.not_sat_iff_forall_mem_ne {α : Type u_1} {a : α → Bool} {c : Clause α} : ¬Sat a c ↔ ∀ (lit : Literal α), lit ∈ c → a lit.fst ≠ lit.snd

theorem Std.Sat.CNF.Clause.sat_of_mem_of_mem_neg {α : Type u_1} {pol : Bool} {c : Clause α} {atom : α} (h1 : (atom, pol) ∈ c) (h2 : (atom, !pol) ∈ c) (a : α → Bool) : Sat a c

theorem Std.Sat.CNF.Clause.unsat_iff_eq_empty {α : Type u_1} {c : Clause α} : c.Unsat ↔ c = empty

def Std.Sat.CNF.eval {α : Type u_1} (a : α → Bool) (f : CNF α) : Bool

Evaluating a CNF formula with respect to an assignment a.

Equations

• Std.Sat.CNF.eval a f = f.clauses.all fun (c : Std.Sat.CNF.Clause α) => Std.Sat.CNF.Clause.eval a c

@[simp]

theorem Std.Sat.CNF.eval_empty {α : Type u_1} (a : α → Bool) : eval a empty = true

@[simp]

theorem Std.Sat.CNF.eval_add {α : Type u_1} {f : CNF α} {c : Clause α} (a : α → Bool) : eval a (f.add c) = (Clause.eval a c && eval a f)

@[simp]

theorem Std.Sat.CNF.eval_append {α : Type u_1} (a : α → Bool) (f1 f2 : CNF α) : eval a (f1 ++ f2) = (eval a f1 && eval a f2)

theorem Std.Sat.CNF.eval_congr {α : Type u_1} (a1 a2 : α → Bool) (f : CNF α) (hw : ∀ (v : α), VarMem v f → a1 v = a2 v) : eval a1 f = eval a2 f

def Std.Sat.CNF.Sat {α : Type u_1} (a : α → Bool) (f : CNF α) : Prop

Equations

• Std.Sat.CNF.Sat a f = (Std.Sat.CNF.eval a f = true)

def Std.Sat.CNF.Unsat {α : Type u_1} (f : CNF α) : Prop

Equations

• f.Unsat = ∀ (a : α → Bool), Std.Sat.CNF.eval a f = false

theorem Std.Sat.CNF.sat_def {α : Type u_1} (a : α → Bool) (f : CNF α) : Sat a f ↔ eval a f = true

theorem Std.Sat.CNF.unsat_def {α : Type u_1} (f : CNF α) : f.Unsat ↔ ∀ (a : α → Bool), eval a f = false

@[simp]

theorem Std.Sat.CNF.not_unsat_empty {α : Type u_1} : ¬empty.Unsat

@[simp]

theorem Std.Sat.CNF.sat_empty {α : Type u_1} {assign : α → Bool} : Sat assign empty

@[simp]

theorem Std.Sat.CNF.sat_add {α : Type u_1} {c : Clause α} {assign : α → Bool} {f : CNF α} : Sat assign (f.add c) ↔ Clause.Sat assign c ∧ Sat assign f

@[simp]

theorem Std.Sat.CNF.sat_append {α : Type u_1} {f1 f2 : CNF α} {assign : α → Bool} : Sat assign (f1 ++ f2) ↔ Sat assign f1 ∧ Sat assign f2

@[simp]

theorem Std.Sat.CNF.unsat_add_empty {α : Type u_1} {g : CNF α} : (g.add Clause.empty).Unsat

theorem Std.Sat.CNF.unsat_iff_not_sat {α : Type u_1} {f : CNF α} : f.Unsat ↔ ∀ (a : α → Bool), ¬Sat a f

theorem Std.Sat.CNF.sat_iff_all_mem_sat {α : Type u_1} {f : CNF α} {a : α → Bool} : Sat a f ↔ ∀ (c : Clause α), c ∈ f → Clause.Sat a c

theorem Std.Sat.CNF.sat_of_all_mem_sat {α : Type u_1} {f : CNF α} {a : α → Bool} : (∀ (c : Clause α), c ∈ f → Clause.Sat a c) → Sat a f

theorem Std.Sat.CNF.sat_of_mem {α : Type u_1} {a : α → Bool} {c : Clause α} {f : CNF α} (h1 : Sat a f) (h2 : c ∈ f) : Clause.Sat a c

theorem Std.Sat.CNF.not_sat_iff_exists_mem_not_sat {α : Type u_1} {a : α → Bool} {f : CNF α} : ¬Sat a f ↔ ∃ (c : Clause α), c ∈ f ∧ ¬Clause.Sat a c

theorem Std.Sat.CNF.unsat_of_mem_unsat {α : Type u_1} {c : Clause α} {f : CNF α} (h1 : c ∈ f) (h2 : c.Unsat) : f.Unsat

theorem Std.Sat.CNF.unsat_add_of_clause_unsat {α : Type u_1} {c : Clause α} {f : CNF α} (h : c.Unsat) : (f.add c).Unsat

theorem Std.Sat.CNF.unsat_add_of_unsat {α : Type u_1} {c : Clause α} {f : CNF α} (h : f.Unsat) : (f.add c).Unsat

theorem Std.Sat.CNF.unsat_append_left {α : Type u_1} {f1 f2 : CNF α} (h : f1.Unsat) : (f1 ++ f2).Unsat

theorem Std.Sat.CNF.unsat_append_right {α : Type u_1} {f1 f2 : CNF α} (h : f2.Unsat) : (f1 ++ f2).Unsat

theorem Std.Sat.CNF.unsat_of_forall_exists {α : Type u_1} {c1 c2 : CNF α} (h : ∀ (a : α → Bool), Sat a c1 → ∃ (a' : α → Bool), Sat a' c2) : c2.Unsat → c1.Unsat