source
@[reducible, inline]
abbrev Std.Sat.CNF.Clause (α : Type u) :
Type u

A clause in a CNF.

The literal `(i, b)` is satisfied if the assignment to `i` agrees with `b`.

Equations

- Std.Sat.CNF.Clause α = List (Std.Sat.Literal α)

Instances For

source
@[reducible, inline]
abbrev Std.Sat.CNF (α : Type u) :
Type u

A CNF formula.

Literals are identified by members of `α`.

Equations

- Std.Sat.CNF α = List (Std.Sat.CNF.Clause α)

Instances For

source
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 = List.any c fun (x : Std.Sat.Literal α) => match x with | (i, n) => a i == n

Instances For

source
@[simp]
theorem Std.Sat.CNF.Clause.eval_nil {α : Type u_1} (a : α → Bool) :
eval a [] = false
source
@[simp]
theorem Std.Sat.CNF.Clause.eval_cons {α : Type u_1} {i : Literal α} {c : List (Literal α)} (a : α → Bool) :
eval a (i :: c) = (a i.fst == i.snd || eval a c)
source
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 = List.all f fun (c : Std.Sat.CNF.Clause α) => Std.Sat.CNF.Clause.eval a c

Instances For

source
@[simp]
theorem Std.Sat.CNF.eval_nil {α : Type u_1} (a : α → Bool) :
eval a [] = true
source
@[simp]
theorem Std.Sat.CNF.eval_cons {α : Type u_1} {c : Clause α} {f : List (Clause α)} (a : α → Bool) :
eval a (c :: f) = (Clause.eval a c && eval a f)
source
@[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)
source
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)

Instances For

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

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

Instances For

source
theorem Std.Sat.CNF.sat_def {α : Type u_1} (a : α → Bool) (f : CNF α) :
Sat a f ↔ eval a f = true
source
theorem Std.Sat.CNF.unsat_def {α : Type u_1} (f : CNF α) :
f.Unsat ↔ ∀ (a : α → Bool), eval a f = false
source
@[simp]
theorem Std.Sat.CNF.not_unsat_nil {α : Type u_1} :
¬Unsat []
source
@[simp]
theorem Std.Sat.CNF.sat_nil {α : Type u_1} {assign : α → Bool} :
Sat assign []
source
@[simp]
theorem Std.Sat.CNF.unsat_nil_cons {α : Type u_1} {g : CNF α} :
Unsat ([] :: g)
source
def Std.Sat.CNF.Clause.Mem {α : Type u_1} (v : α) (c : Clause α) :
Prop

Variable `v` occurs in `Clause` `c`.

Equations

- Std.Sat.CNF.Clause.Mem v c = ((v, false) ∈ c ∨ (v, true) ∈ c)

Instances For

source
instance Std.Sat.CNF.Clause.instDecidableMemOfDecidableEq {α : Type u_1} {v : α} {c : Clause α} [DecidableEq α] :
Decidable (Mem v c)
Equations

- Std.Sat.CNF.Clause.instDecidableMemOfDecidableEq = inferInstanceAs (Decidable ((v, false) ∈ c ∨ (v, true) ∈ c))

source
@[simp]
theorem Std.Sat.CNF.Clause.not_mem_nil {α : Type u_1} {v : α} :
¬Mem v []
source
@[simp]
theorem Std.Sat.CNF.Clause.mem_cons {α : Type u_1} {l : Literal α} {c : List (Literal α)} {v : α} :
Mem v (l :: c) ↔ v = l.fst ∨ Mem v c
source
theorem Std.Sat.CNF.Clause.mem_of {α✝ : Type u_1} {c : Clause α✝} {v : α✝} {p : Bool} (h : (v, p) ∈ c) :
Mem v c
source
theorem Std.Sat.CNF.Clause.eval_congr {α : Type u_1} (a1 a2 : α → Bool) (c : Clause α) (hw : ∀ (i : α), Mem i c → a1 i = a2 i) :
eval a1 c = eval a2 c
source
def Std.Sat.CNF.Mem {α : Type u_1} (v : α) (f : CNF α) :
Prop

Variable `v` occurs in `CNF` formula `f`.

Equations

- Std.Sat.CNF.Mem v f = ∃ (c : Std.Sat.CNF.Clause α), c ∈ f ∧ Std.Sat.CNF.Clause.Mem v c

Instances For

source
instance Std.Sat.CNF.instDecidableMemOfDecidableEq {α : Type u_1} {v : α} {f : CNF α} [DecidableEq α] :
Decidable (Mem v f)
Equations

- Std.Sat.CNF.instDecidableMemOfDecidableEq = inferInstanceAs (Decidable (∃ (x : Std.Sat.CNF.Clause α), x ∈ f ∧ Std.Sat.CNF.Clause.Mem v x))

source
theorem Std.Sat.CNF.any_not_isEmpty_iff_exists_mem {α : Type u_1} {f : CNF α} :
(List.any f fun (c : Clause α) => !List.isEmpty c) = true ↔ ∃ (v : α), Mem v f
source
theorem Std.Sat.CNF.not_exists_mem {α✝ : Type u_1} {f : CNF α✝} :
(¬∃ (v : α✝), Mem v f) ↔ ∃ (n : Nat), f = List.replicate n []
source
instance Std.Sat.CNF.instDecidableExistsMemOfDecidableEq {α : Type u_1} {f : CNF α} [DecidableEq α] :
Decidable (∃ (v : α), Mem v f)
Equations

- Std.Sat.CNF.instDecidableExistsMemOfDecidableEq = decidable_of_iff ((List.any f fun (c : Std.Sat.CNF.Clause α) => !List.isEmpty c) = true) ⋯

source
theorem Std.Sat.CNF.not_mem_nil {α : Type u_1} {v : α} :
¬Mem v []
source
theorem Std.Sat.CNF.mem_cons {α : Type u_1} {v : α} {c : Clause α} {f : CNF α} :
Mem v (c :: f) ↔ Clause.Mem v c ∨ Mem v f
source
theorem Std.Sat.CNF.mem_of {α✝ : Type u_1} {f : CNF α✝} {c : Clause α✝} {v : α✝} (h : c ∈ f) (w : Clause.Mem v c) :
Mem v f
source
@[simp]
theorem Std.Sat.CNF.mem_append {α : Type u_1} {v : α} {f1 f2 : CNF α} :
Mem v (f1 ++ f2) ↔ Mem v f1 ∨ Mem v f2
source
theorem Std.Sat.CNF.eval_congr {α : Type u_1} (a1 a2 : α → Bool) (f : CNF α) (hw : ∀ (v : α), Mem v f → a1 v = a2 v) :
eval a1 f = eval a2 f