This module contains an implementation of a verified Tseitin transformation on AIGs. The key results are the toCNF function and the toCNF_equisat correctness statement. The implementation is done in the style of section 3.4 of the AIGNET paper.

def Std.Sat.AIG.Decl.constToCNF {α : Type u_1} (output : α) (const : Bool) : Std.Sat.CNF α

Produce a Tseitin style CNF for a Decl.const, using output as the tree node variable.

Equations

• Std.Sat.AIG.Decl.constToCNF output const = [[(output, const)]]

def Std.Sat.AIG.Decl.atomToCNF {α : Type u_1} (output atom : α) : Std.Sat.CNF α

Produce a Tseitin style CNF for a Decl.atom, using output as the tree node variable.

Equations

• Std.Sat.AIG.Decl.atomToCNF output atom = [[(output, true), (atom, false)], [(output, false), (atom, true)]]

def Std.Sat.AIG.Decl.gateToCNF {α : Type u_1} (output lhs rhs : α) (linv rinv : Bool) : Std.Sat.CNF α

Produce a Tseitin style CNF for a Decl.gate, using output as the tree node variable.

Equations

• Std.Sat.AIG.Decl.gateToCNF output lhs rhs linv rinv = [[(output, false), (lhs, !linv)], [(output, false), (rhs, !rinv)], [(output, true), (lhs, linv), (rhs, rinv)]]

@[simp]

theorem Std.Sat.AIG.Decl.constToCNF_eval {α✝ : Type u_1} {output : α✝} {b : Bool} {assign : α✝ → Bool} : Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.constToCNF output b) = (assign output == b)

@[simp]

theorem Std.Sat.AIG.Decl.atomToCNF_eval {α✝ : Type u_1} {output a : α✝} {assign : α✝ → Bool} : Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.atomToCNF output a) = (assign output == assign a)

@[simp]

theorem Std.Sat.AIG.Decl.gateToCNF_eval {α✝ : Type u_1} {output lhs rhs : α✝} {linv rinv : Bool} {assign : α✝ → Bool} : Std.Sat.CNF.eval assign (Std.Sat.AIG.Decl.gateToCNF output lhs rhs linv rinv) = (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))

@[reducible, inline]

abbrev Std.Sat.AIG.CNFVar (aig : Std.Sat.AIG Nat) : Type

Equations

• aig.CNFVar = (Nat ⊕ Fin aig.decls.size)

def Std.Sat.AIG.toCNF.mixAssigns {aig : Std.Sat.AIG Nat} (assign1 : Nat → Bool) (assign2 : Fin aig.decls.size → Bool) : aig.CNFVar → Bool

Mix:

1. An assignment for AIG atoms
2. An assignment for auxiliary Tseitin variables into an assignment that can be used by a CNF produced by our Tseitin transformation.

Equations

• Std.Sat.AIG.toCNF.mixAssigns assign1 assign2 (Sum.inl var) = assign1 var
• Std.Sat.AIG.toCNF.mixAssigns assign1 assign2 (Sum.inr var) = assign2 var

def Std.Sat.AIG.toCNF.projectLeftAssign {aig : Std.Sat.AIG Nat} (assign : aig.CNFVar → Bool) : Nat → Bool

Project the atom assignment out of a CNF assignment

Equations

• Std.Sat.AIG.toCNF.projectLeftAssign assign x✝ = assign (Sum.inl x✝)

def Std.Sat.AIG.toCNF.projectRightAssign {aig : Std.Sat.AIG Nat} (assign : aig.CNFVar → Bool) (idx : Nat) : idx < aig.decls.size → Bool

Project the auxiliary variable assignment out of a CNF assignment

Equations

• Std.Sat.AIG.toCNF.projectRightAssign assign idx h = assign (Sum.inr ⟨idx, h⟩)

@[simp]

theorem Std.Sat.AIG.toCNF.projectLeftAssign_property {aig✝ : Std.Sat.AIG Nat} {assign : aig✝.CNFVar → Bool} {x : Nat} : Std.Sat.AIG.toCNF.projectLeftAssign assign x = assign (Sum.inl x)

@[simp]

theorem Std.Sat.AIG.toCNF.projectRightAssign_property {aig✝ : Std.Sat.AIG Nat} {assign : aig✝.CNFVar → Bool} {x : Nat} {hx : x < aig✝.decls.size} : Std.Sat.AIG.toCNF.projectRightAssign assign x hx = assign (Sum.inr ⟨x, hx⟩)

def Std.Sat.AIG.toCNF.cnfSatAssignment (aig : Std.Sat.AIG Nat) (assign1 : Nat → Bool) : aig.CNFVar → Bool

Given an atom assignment, produce an assignment that will always satisfy the CNF generated by our Tseitin transformation. This is done by combining the atom assignment with an assignment for the auxiliary variables, that just evaluates the AIG at the corresponding node.

Equations

• Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1 = Std.Sat.AIG.toCNF.mixAssigns assign1 fun (idx : Fin aig.decls.size) => ⟦assign1, { aig := aig, ref := { gate := ↑idx, hgate := ⋯ } }⟧

@[simp]

theorem Std.Sat.AIG.toCNF.satAssignment_inl {aig : Std.Sat.AIG Nat} {assign1 : Nat → Bool} {x : Nat} : Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1 (Sum.inl x) = assign1 x

@[simp]

theorem Std.Sat.AIG.toCNF.satAssignment_inr {aig : Std.Sat.AIG Nat} {assign1 : Nat → Bool} {x : Fin aig.decls.size} : Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1 (Sum.inr x) = ⟦assign1, { aig := aig, ref := { gate := ↑x, hgate := ⋯ } }⟧

structure Std.Sat.AIG.toCNF.Cache.Inv {aig : Std.Sat.AIG Nat} (cnf : Std.Sat.CNF aig.CNFVar) (marks : Array Bool) (hmarks : marks.size = aig.decls.size) : Prop

The central invariants for the Cache.

• hmark (lhs rhs : Nat) (linv rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size) (_hmarked : marks[idx] = true) (heq : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) : marks[lhs] = true ∧ marks[rhs] = true

  If there exists an AIG node that is marked, its children are also guaranteed to be marked already. This allows us to conclude that if a gate node is marked, all of its (transitive) children are also marked.

• heval (assign : aig.CNFVar → Bool) (_heval : Std.Sat.CNF.eval assign cnf = true) (idx : Nat) (hbound : idx < aig.decls.size) (_hmark : marks[idx] = true) : ⟦Std.Sat.AIG.toCNF.projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ = Std.Sat.AIG.toCNF.projectRightAssign assign idx hbound

  Relate satisfiability results about our produced CNF to satisfiability results about the AIG that we are processing. The intuition for this is: if a node is marked, its CNF (and all required children CNFs according to hmark) are already part of the current CNF. Thus the current CNF is already mirroring the semantics of the marked node. This means that if the CNF is satisfiable at some assignment, we can evaluate the marked node under the atom part of that assignment and will get the value that was assigned to the corresponding auxiliary variable as a result.

theorem Std.Sat.AIG.toCNF.Cache.Inv_init {aig : Std.Sat.AIG Nat} : Std.Sat.AIG.toCNF.Cache.Inv [] (mkArray aig.decls.size false) ⋯

The Cache invariant always holds for an empty CNF when all nodes are unmarked.

structure Std.Sat.AIG.toCNF.Cache (aig : Std.Sat.AIG Nat) (cnf : Std.Sat.CNF aig.CNFVar) : Type

The CNF cache. It keeps track of AIG nodes that we already turned into CNF to avoid adding the same CNF twice.

• marks : Array Bool

  Keeps track of AIG nodes that we already turned into CNF.

• hmarks : self.marks.size = aig.decls.size

  There are always as many marks as AIG nodes.

• inv : Std.Sat.AIG.toCNF.Cache.Inv cnf self.marks ⋯

  The invariant to make sure that marks is well formed with respect to the cnf

structure Std.Sat.AIG.toCNF.Cache.IsExtensionBy {aig : Std.Sat.AIG Nat} {cnf1 cnf2 : Std.Sat.CNF aig.CNFVar} (cache1 : Std.Sat.AIG.toCNF.Cache aig cnf1) (cache2 : Std.Sat.AIG.toCNF.Cache aig cnf2) (new : Nat) (hnew : new < aig.decls.size) : Prop

We say that a cache extends another by an index when it doesn't invalidate any entry and has an entry for that index.

• extension (idx : Nat) (hidx : idx < aig.decls.size) : cache1.marks[idx] = true → cache2.marks[idx] = true

  No entry is invalidated.

• trueAt : cache2.marks[new] = true

  The second cache is true at the new index.

theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_trans_left {aig : Std.Sat.AIG Nat} {cnf1 cnf2 cnf3 : Std.Sat.CNF aig.CNFVar} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (cache1 : Std.Sat.AIG.toCNF.Cache aig cnf1) (cache2 : Std.Sat.AIG.toCNF.Cache aig cnf2) (cache3 : Std.Sat.AIG.toCNF.Cache aig cnf3) (h12 : cache1.IsExtensionBy cache2 new1 hnew1) (h23 : cache2.IsExtensionBy cache3 new2 hnew2) : cache1.IsExtensionBy cache3 new1 hnew1

theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_trans_right {aig : Std.Sat.AIG Nat} {cnf1 cnf2 cnf3 : Std.Sat.CNF aig.CNFVar} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (cache1 : Std.Sat.AIG.toCNF.Cache aig cnf1) (cache2 : Std.Sat.AIG.toCNF.Cache aig cnf2) (cache3 : Std.Sat.AIG.toCNF.Cache aig cnf3) (h12 : cache1.IsExtensionBy cache2 new1 hnew1) (h23 : cache2.IsExtensionBy cache3 new2 hnew2) : cache1.IsExtensionBy cache3 new2 hnew2

theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_rfl {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {idx : Nat} {omega : idx < aig.decls.size} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) {h : idx < cache.marks.size} (hmarked : cache.marks[idx] = true) : cache.IsExtensionBy cache idx ⋯

Cache extension is a reflexive relation.

theorem Std.Sat.AIG.toCNF.Cache.IsExtensionBy_set {aig : Std.Sat.AIG Nat} {cnf1 cnf2 : Std.Sat.CNF aig.CNFVar} (cache1 : Std.Sat.AIG.toCNF.Cache aig cnf1) (cache2 : Std.Sat.AIG.toCNF.Cache aig cnf2) (idx : Nat) (hbound : idx < cache1.marks.size) (h : cache2.marks = cache1.marks.set idx true hbound) : cache1.IsExtensionBy cache2 idx ⋯

def Std.Sat.AIG.toCNF.Cache.init (aig : Std.Sat.AIG Nat) : Std.Sat.AIG.toCNF.Cache aig []

A cache with no entries is valid for an empty CNF.

Equations

• Std.Sat.AIG.toCNF.Cache.init aig = { marks := mkArray aig.decls.size false, hmarks := ⋯, inv := ⋯ }

def Std.Sat.AIG.toCNF.Cache.addConst {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {b : Bool} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.const b) : { out : Std.Sat.AIG.toCNF.Cache aig (Std.Sat.AIG.Decl.constToCNF (Sum.inr ⟨idx, h⟩) b ++ cnf) // cache.IsExtensionBy out idx h }

Add a Decl.const to a Cache.

Equations

• cache.addConst idx h htip = ⟨{ marks := cache.marks.set idx true ⋯, hmarks := ⋯, inv := ⋯ }, ⋯⟩

def Std.Sat.AIG.toCNF.Cache.addAtom {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {a : Nat} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.atom a) : { out : Std.Sat.AIG.toCNF.Cache aig (Std.Sat.AIG.Decl.atomToCNF (Sum.inr ⟨idx, h⟩) (Sum.inl a) ++ cnf) // cache.IsExtensionBy out idx h }

Add a Decl.atom to a cache.

Equations

• cache.addAtom idx h htip = ⟨{ marks := cache.marks.set idx true ⋯, hmarks := ⋯, inv := ⋯ }, ⋯⟩

def Std.Sat.AIG.toCNF.Cache.addGate {aig : Std.Sat.AIG Nat} {cnf : Std.Sat.CNF aig.CNFVar} {lhs rhs : Nat} {linv rinv : Bool} (cache : Std.Sat.AIG.toCNF.Cache aig cnf) {hlb : lhs < cache.marks.size} {hrb : rhs < cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) (hl : cache.marks[lhs] = true) (hr : cache.marks[rhs] = true) : { out : Std.Sat.AIG.toCNF.Cache aig (Std.Sat.AIG.Decl.gateToCNF (Sum.inr ⟨idx, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv ++ cnf) // cache.IsExtensionBy out idx h }

Add a Decl.gate to a cache.

Equations

• cache.addGate idx h htip hl hr = ⟨{ marks := cache.marks.set idx true ⋯, hmarks := ⋯, inv := ⋯ }, ⋯⟩

def Std.Sat.AIG.toCNF.State.Inv {aig : Std.Sat.AIG Nat} (cnf : Std.Sat.CNF aig.CNFVar) : Prop

The key invariant about the State itself (without cache): The CNF we produce is always satisfiable at cnfSatAssignment.

Equations

• Std.Sat.AIG.toCNF.State.Inv cnf = ∀ (assign1 : Nat → Bool), Std.Sat.CNF.Sat (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) cnf

theorem Std.Sat.AIG.toCNF.State.Inv_nil {aig : Std.Sat.AIG Nat} : Std.Sat.AIG.toCNF.State.Inv []

The State invariant always holds when we have an empty CNF.

theorem Std.Sat.AIG.toCNF.State.Inv_append {aig✝ : Std.Sat.AIG Nat} {cnf1 cnf2 : Std.Sat.CNF aig✝.CNFVar} (h1 : Std.Sat.AIG.toCNF.State.Inv cnf1) (h2 : Std.Sat.AIG.toCNF.State.Inv cnf2) : Std.Sat.AIG.toCNF.State.Inv (cnf1 ++ cnf2)

Combining two CNFs for which State.Inv holds preserves State.Inv.

theorem Std.Sat.AIG.toCNF.State.Inv_constToCNF {upper : Nat} {aig : Std.Sat.AIG Nat} {h : upper < aig.decls.size} {b : Bool} (heq : aig.decls[upper] = Std.Sat.AIG.Decl.const b) : Std.Sat.AIG.toCNF.State.Inv (Std.Sat.AIG.Decl.constToCNF (Sum.inr ⟨upper, h⟩) b)

State.Inv holds for the CNF that we produce for a Decl.const.

theorem Std.Sat.AIG.toCNF.State.Inv_atomToCNF {upper : Nat} {aig : Std.Sat.AIG Nat} {h : upper < aig.decls.size} {a : Nat} (heq : aig.decls[upper] = Std.Sat.AIG.Decl.atom a) : Std.Sat.AIG.toCNF.State.Inv (Std.Sat.AIG.Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a))

State.Inv holds for the CNF that we produce for a Decl.atom

theorem Std.Sat.AIG.toCNF.State.Inv_gateToCNF {upper lhs rhs : Nat} {linv rinv : Bool} {aig : Std.Sat.AIG Nat} {h : upper < aig.decls.size} (heq : aig.decls[upper] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) : Std.Sat.AIG.toCNF.State.Inv (Std.Sat.AIG.Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs, ⋯⟩) (Sum.inr ⟨rhs, ⋯⟩) linv rinv)

State.Inv holds for the CNF that we produce for a Decl.gate

structure Std.Sat.AIG.toCNF.State (aig : Std.Sat.AIG Nat) : Type

The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.

• cnf : Std.Sat.CNF aig.CNFVar

  The CNF clauses so far.

• cache : Std.Sat.AIG.toCNF.Cache aig self.cnf

  A cache so that we don't generate CNF for an AIG node more than once.

• inv : Std.Sat.AIG.toCNF.State.Inv self.cnf

  The invariant that cnf has to maintain as we build it up.

def Std.Sat.AIG.toCNF.State.empty (aig : Std.Sat.AIG Nat) : Std.Sat.AIG.toCNF.State aig

An initial state with no CNF clauses and an empty cache.

Equations

• Std.Sat.AIG.toCNF.State.empty aig = { cnf := [], cache := Std.Sat.AIG.toCNF.Cache.init aig, inv := ⋯ }

@[reducible, inline]

abbrev Std.Sat.AIG.toCNF.State.IsExtensionBy {aig : Std.Sat.AIG Nat} (state1 state2 : Std.Sat.AIG.toCNF.State aig) (new : Nat) (hnew : new < aig.decls.size) : Prop

State extension are Cache.IsExtensionBy for now.

Equations

• state1.IsExtensionBy state2 new hnew = state1.cache.IsExtensionBy state2.cache new hnew

theorem Std.Sat.AIG.toCNF.State.IsExtensionBy_trans_left {aig : Std.Sat.AIG Nat} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (state1 state2 state3 : Std.Sat.AIG.toCNF.State aig) (h12 : state1.IsExtensionBy state2 new1 hnew1) (h23 : state2.IsExtensionBy state3 new2 hnew2) : state1.IsExtensionBy state3 new1 hnew1

theorem Std.Sat.AIG.toCNF.State.IsExtensionBy_trans_right {aig : Std.Sat.AIG Nat} {new1 : Nat} {hnew1 : new1 < aig.decls.size} {new2 : Nat} {hnew2 : new2 < aig.decls.size} (state1 state2 state3 : Std.Sat.AIG.toCNF.State aig) (h12 : state1.IsExtensionBy state2 new1 hnew1) (h23 : state2.IsExtensionBy state3 new2 hnew2) : state1.IsExtensionBy state3 new2 hnew2

theorem Std.Sat.AIG.toCNF.State.IsExtensionBy_rfl {aig : Std.Sat.AIG Nat} {idx : Nat} {omega : idx < aig.decls.size} (state : Std.Sat.AIG.toCNF.State aig) {h : idx < state.cache.marks.size} (hmarked : state.cache.marks[idx] = true) : state.IsExtensionBy state idx ⋯

State extension is a reflexive relation.

def Std.Sat.AIG.toCNF.State.addConst {aig : Std.Sat.AIG Nat} {b : Bool} (state : Std.Sat.AIG.toCNF.State aig) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.const b) : { out : Std.Sat.AIG.toCNF.State aig // state.IsExtensionBy out idx h }

Add the CNF for a Decl.const to the state.

Equations

• One or more equations did not get rendered due to their size.

def Std.Sat.AIG.toCNF.State.addAtom {aig : Std.Sat.AIG Nat} {a : Nat} (state : Std.Sat.AIG.toCNF.State aig) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.atom a) : { out : Std.Sat.AIG.toCNF.State aig // state.IsExtensionBy out idx h }

Add the CNF for a Decl.atom to the state.

Equations

• One or more equations did not get rendered due to their size.

def Std.Sat.AIG.toCNF.State.addGate {aig : Std.Sat.AIG Nat} {lhs rhs : Nat} {linv rinv : Bool} (state : Std.Sat.AIG.toCNF.State aig) {hlb : lhs < state.cache.marks.size} {hrb : rhs < state.cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Std.Sat.AIG.Decl.gate lhs rhs linv rinv) (hl : state.cache.marks[lhs] = true) (hr : state.cache.marks[rhs] = true) : { out : Std.Sat.AIG.toCNF.State aig // state.IsExtensionBy out idx h }

Add the CNF for a Decl.gate to the state.

Equations

• One or more equations did not get rendered due to their size.

def Std.Sat.AIG.toCNF.State.eval {aig : Std.Sat.AIG Nat} (assign : aig.CNFVar → Bool) (state : Std.Sat.AIG.toCNF.State aig) : Bool

Evaluate the CNF contained within the state.

Equations

• Std.Sat.AIG.toCNF.State.eval assign state = Std.Sat.CNF.eval assign state.cnf

def Std.Sat.AIG.toCNF.State.Sat {aig : Std.Sat.AIG Nat} (assign : aig.CNFVar → Bool) (state : Std.Sat.AIG.toCNF.State aig) : Prop

The CNF within the state is sat.

Equations

• Std.Sat.AIG.toCNF.State.Sat assign state = Std.Sat.CNF.Sat assign state.cnf

def Std.Sat.AIG.toCNF.State.Unsat {aig : Std.Sat.AIG Nat} (state : Std.Sat.AIG.toCNF.State aig) : Prop

The CNF within the state is unsat.

Equations

• state.Unsat = state.cnf.Unsat

theorem Std.Sat.AIG.toCNF.State.sat_def {aig : Std.Sat.AIG Nat} (assign : aig.CNFVar → Bool) (state : Std.Sat.AIG.toCNF.State aig) : Std.Sat.AIG.toCNF.State.Sat assign state ↔ Std.Sat.CNF.Sat assign state.cnf

theorem Std.Sat.AIG.toCNF.State.unsat_def {aig : Std.Sat.AIG Nat} (state : Std.Sat.AIG.toCNF.State aig) : state.Unsat ↔ state.cnf.Unsat

@[simp]

theorem Std.Sat.AIG.toCNF.State.eval_eq {aig✝ : Std.Sat.AIG Nat} {assign : aig✝.CNFVar → Bool} {state : Std.Sat.AIG.toCNF.State aig✝} : Std.Sat.AIG.toCNF.State.eval assign state = Std.Sat.CNF.eval assign state.cnf

@[simp]

theorem Std.Sat.AIG.toCNF.State.sat_iff {aig✝ : Std.Sat.AIG Nat} {assign : aig✝.CNFVar → Bool} {state : Std.Sat.AIG.toCNF.State aig✝} : Std.Sat.AIG.toCNF.State.Sat assign state ↔ Std.Sat.CNF.Sat assign state.cnf

@[simp]

theorem Std.Sat.AIG.toCNF.State.unsat_iff {aig✝ : Std.Sat.AIG Nat} {state : Std.Sat.AIG.toCNF.State aig✝} : state.Unsat ↔ state.cnf.Unsat

def Std.Sat.AIG.toCNF (entry : Std.Sat.AIG.Entrypoint Nat) : Std.Sat.CNF Nat

Convert an AIG into CNF, starting at some entry node.

Equations

• One or more equations did not get rendered due to their size.

def Std.Sat.AIG.toCNF.inj {aig : Std.Sat.AIG Nat} (var : aig.CNFVar) : Nat

Equations

• Std.Sat.AIG.toCNF.inj (Sum.inl var_1) = aig.decls.size + var_1
• Std.Sat.AIG.toCNF.inj (Sum.inr var_1) = ↑var_1

@[irreducible]

def Std.Sat.AIG.toCNF.go (aig : Std.Sat.AIG Nat) (upper : Nat) (h : upper < aig.decls.size) (state : Std.Sat.AIG.toCNF.State aig) : { out : Std.Sat.AIG.toCNF.State aig // state.IsExtensionBy out upper h }

Equations

• One or more equations did not get rendered due to their size.

theorem Std.Sat.AIG.toCNF.inj_is_injection {aig : Std.Sat.AIG Nat} (a b : aig.CNFVar) : Std.Sat.AIG.toCNF.inj a = Std.Sat.AIG.toCNF.inj b → a = b

The function we use to convert from CNF with explicit auxiliary variables to just Nat variables in toCNF is an injection.

theorem Std.Sat.AIG.toCNF.go_marks {aig : Std.Sat.AIG Nat} {start : Nat} {h : start < aig.decls.size} {state : Std.Sat.AIG.toCNF.State aig} : (Std.Sat.AIG.toCNF.go aig start h state).val.cache.marks[start] = true

The node that we started CNF conversion at will always be marked as visited in the CNF cache.

theorem Std.Sat.AIG.toCNF.go_sat (aig : Std.Sat.AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) (state : Std.Sat.AIG.toCNF.State aig) : Std.Sat.AIG.toCNF.State.Sat (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) (Std.Sat.AIG.toCNF.go aig start h1 state).val

The CNF returned by go will always be SAT at cnfSatAssignment.

theorem Std.Sat.AIG.toCNF.go_as_denote' (aig : Std.Sat.AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) : ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true → Std.Sat.AIG.toCNF.State.eval (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) (Std.Sat.AIG.toCNF.go aig start h1 (Std.Sat.AIG.toCNF.State.empty aig)).val = true

theorem Std.Sat.AIG.toCNF.go_as_denote {sat? : Bool} (aig : Std.Sat.AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) : (⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ && Std.Sat.AIG.toCNF.State.eval (Std.Sat.AIG.toCNF.cnfSatAssignment aig assign1) (Std.Sat.AIG.toCNF.go aig start h1 (Std.Sat.AIG.toCNF.State.empty aig)).val) = sat? → ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = sat?

Connect SAT results about the CNF to SAT results about the AIG.

theorem Std.Sat.AIG.toCNF.denote_as_go {aig : Std.Sat.AIG Nat} {start : Nat} {h1 : start < aig.decls.size} {assign : aig.CNFVar → Bool} : ⟦Std.Sat.AIG.toCNF.projectLeftAssign assign, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = false → Std.Sat.CNF.eval assign ([(Sum.inr ⟨start, h1⟩, true)] :: (Std.Sat.AIG.toCNF.go aig start h1 (Std.Sat.AIG.toCNF.State.empty aig)).val.cnf) = false

Connect SAT results about the AIG to SAT results about the CNF.

theorem Std.Sat.AIG.toCNF_equisat (entry : Std.Sat.AIG.Entrypoint Nat) : (Std.Sat.AIG.toCNF entry).Unsat ↔ entry.Unsat

An AIG is unsat iff its CNF is unsat.