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.toCNF.Cache.Inv {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (cnf : CNF Nat) (marks : Array Bool) (hmarks : marks.size = aig.decls.size) : Prop

The central invariant for the Cache.

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 is 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 variable of the node as a result.

Equations

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

structure Std.Sat.AIG.toCNF.Cache {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (cnf : CNF Nat) : 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 : Inv aig cnf self.marks ⋯

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

def Std.Sat.AIG.toCNF.State.Inv {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) (cnf : CNF Nat) : Prop

The key invariant about the State itself (without cache): The CNF we produce is always satisfied by any assignment that evaluates the AIG at the variable of each node, in particular by cnfSatAssignment.

Note that this definition leaves variables that do not occur in the AIG unconstrained so that the CNF can be reused for an AIG that extends the current one.

Equations

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

structure Std.Sat.AIG.toCNF.State {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) : Type

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

• cnf : CNF Nat

  The CNF clauses so far.

• cache : Cache aig self.cnf

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

• inv : Inv aig self.cnf

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

def Std.Sat.AIG.toCNF.State.empty {α : Type} [Hashable α] [DecidableEq α] (aig : AIG α) : State aig

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

Equations

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

def Std.Sat.AIG.toCNF.State.cast {α : Type} [Hashable α] [DecidableEq α] {aig1 aig2 : AIG α} (state : State aig1) (hprefix : IsPrefix aig1.decls aig2.decls) : State aig2

Reuse a State for an AIG that extends the original one, see Cache.cast.

Equations

• state.cast hprefix = { cnf := state.cnf, cache := Std.Sat.AIG.toCNF.Cache.cast✝ state.cache hprefix, inv := ⋯ }

def Std.Sat.AIG.toCNF' {α : Type} [Hashable α] [DecidableEq α] (entry : Entrypoint α) (state : toCNF.State entry.aig) : toCNF.State entry.aig

Equations

• Std.Sat.AIG.toCNF' entry state = match Std.Sat.AIG.toCNF'.go✝ entry.aig entry.ref.gate ⋯ state with | ⟨state_1, property⟩ => state_1

@[inline]

def Std.Sat.AIG.toCNF {α : Type} [Hashable α] [DecidableEq α] (entry : Entrypoint α) : CNF Nat

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

Equations

• Std.Sat.AIG.toCNF entry = (Std.Sat.AIG.toCNF' entry (Std.Sat.AIG.toCNF.State.empty entry.aig)).cnf.add (Std.Sat.CNF.Clause.empty.add entry.ref.gate !entry.ref.invert)

theorem Std.Sat.AIG.toCNF_equisat {α : Type} [Hashable α] [DecidableEq α] (entry : Entrypoint α) : (toCNF entry).Unsat ↔ entry.Unsat

An AIG is unsat iff its CNF is unsat.