@[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 α)

structure Std.Sat.CNF (α : Type u) : Type u

A CNF formula.

Literals are identified by members of α.

• clauses : Array (Clause α)

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

@[simp]

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

@[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)

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

@[inline]

def Std.Sat.CNF.empty {α : Type u_1} : CNF α

Equations

• Std.Sat.CNF.empty = { clauses := #[] }

@[inline]

def Std.Sat.CNF.emptyWithCapacity {α : Type u_1} (n : Nat) : CNF α

Equations

• Std.Sat.CNF.emptyWithCapacity n = { clauses := Array.emptyWithCapacity n }

@[inline]

def Std.Sat.CNF.add {α : Type u_1} (c : Clause α) (f : CNF α) : CNF α

Equations

• Std.Sat.CNF.add c f = { clauses := f.clauses.push c }

@[inline]

def Std.Sat.CNF.append {α : Type u_1} (f1 f2 : CNF α) : CNF α

Equations

• f1.append f2 = { clauses := f1.clauses ++ f2.clauses }

@[implicit_reducible]

instance Std.Sat.CNF.instAppend {α : Type u_1} : Append (CNF α)

Equations

• Std.Sat.CNF.instAppend = { append := Std.Sat.CNF.append }

@[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 (add c f) = (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)

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.unsat_add_nil {α : Type u_1} {g : CNF α} : (add [] g).Unsat

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)

@[implicit_reducible]

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))

@[simp]

theorem Std.Sat.CNF.Clause.not_mem_nil {α : Type u_1} {v : α} : ¬Mem v []

@[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

theorem Std.Sat.CNF.Clause.mem_of {α✝ : Type u_1} {c : Clause α✝} {v : α✝} {p : Bool} (h : (v, p) ∈ c) : Mem v c

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

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

Clause c occurs in CNF formula f.

Equations

• f.Mem c = (c ∈ f.clauses)

@[implicit_reducible]

instance Std.Sat.CNF.instMembershipClause {α : Type u_1} : Membership (Clause α) (CNF α)

Equations

• Std.Sat.CNF.instMembershipClause = { mem := Std.Sat.CNF.Mem }

@[implicit_reducible]

instance Std.Sat.CNF.instDecidableMemClauseOfDecidableEq {α : Type u_1} {c : Clause α} {f : CNF α} [DecidableEq α] : Decidable (c ∈ f)

Equations

• Std.Sat.CNF.instDecidableMemClauseOfDecidableEq = inferInstanceAs (Decidable (c ∈ f.clauses))

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

Variable v occurs in CNF formula f.

Equations

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

@[implicit_reducible]

instance Std.Sat.CNF.instDecidableVarMemOfDecidableEq {α : Type u_1} {v : α} {f : CNF α} [DecidableEq α] : Decidable (VarMem v f)

Equations

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

theorem Std.Sat.CNF.Internal.any_not_isEmpty_iff_exists_mem {α : Type u_1} {f : CNF α} : (f.clauses.any fun (c : Clause α) => !List.isEmpty c) = true ↔ ∃ (v : α), VarMem v f

@[implicit_reducible]

instance Std.Sat.CNF.instDecidableExistsVarMemOfDecidableEq {α : Type u_1} {f : CNF α} [DecidableEq α] : Decidable (∃ (v : α), VarMem v f)

Equations

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

theorem Std.Sat.CNF.not_VarMem_empty {α : Type u_1} {v : α} : ¬VarMem v empty

theorem Std.Sat.CNF.VarMem_add {α : Type u_1} {v : α} {c : Clause α} {f : CNF α} : VarMem v (add c f) ↔ Clause.Mem v c ∨ VarMem v f

theorem Std.Sat.CNF.VarMem_of {α✝ : Type u_1} {f : CNF α✝} {c : Clause α✝} {v : α✝} (h : c ∈ f) (w : Clause.Mem v c) : VarMem v f

theorem Std.Sat.CNF.Internal.mem_iff {α : Type u_1} {c : Clause α} {f : CNF α} : c ∈ f ↔ c ∈ f.clauses

theorem Std.Sat.CNF.Internal.clauses_append {α : Type u_1} {f1 f2 : CNF α} : (f1 ++ f2).clauses = f1.clauses ++ f2.clauses

theorem Std.Sat.CNF.Internal.ext_iff {α : Type u_1} {f1 f2 : CNF α} : f1 = f2 ↔ f1.clauses = f2.clauses

@[simp]

theorem Std.Sat.CNF.emptyWithCapacity_eq_empty {α : Type u_1} (n : Nat) : emptyWithCapacity n = empty

@[simp]

theorem Std.Sat.CNF.VarMem_append {α : Type u_1} {v : α} {f1 f2 : CNF α} : VarMem v (f1 ++ f2) ↔ VarMem v f1 ∨ VarMem v 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