Std.Sat.AIG.CNF

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.

source

def Std.Sat.AIG.Decl.falseToCNF {α : Type u_1} (output : α) :

CNF α

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

Equations

Instances For

source

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

CNF α

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

Equations

Instances For

source

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

CNF α

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

Equations

Instances For

source

@[simp]

theorem Std.Sat.AIG.Decl.falseToCNF_eval {α✝ : Type u_1} {output : α✝} {assign : α✝ → Bool} :

CNF.eval assign (falseToCNF output) = (assign output == Bool.false)

source

@[simp]

theorem Std.Sat.AIG.Decl.atomToCNF_eval {α✝ : Type u_1} {output a : α✝} {assign : α✝ → Bool} :

CNF.eval assign (atomToCNF output a) = (assign output == assign a)

source

@[simp]

theorem Std.Sat.AIG.Decl.gateToCNF_eval {α✝ : Type u_1} {output lhs rhs : α✝} {linv rinv : Bool} {assign : α✝ → Bool} :

CNF.eval assign (gateToCNF output lhs rhs linv rinv) = (assign output == ((assign lhs ^^ linv) && (assign rhs ^^ rinv)))

source

@[reducible, inline]

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

Type

Equations

Instances For

source

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

aig.CNFVar → Bool

Mix:

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

Equations

Instances For

source

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

Nat → Bool

Project the atom assignment out of a CNF assignment

Equations

Instances For

source

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

idx < aig.decls.size → Bool

Project the auxiliary variable assignment out of a CNF assignment

Equations

Instances For

source

@[simp]

theorem Std.Sat.AIG.toCNF.projectLeftAssign_property {aig✝ : AIG Nat} {assign : aig✝.CNFVar → Bool} {x : Nat} :

projectLeftAssign assign x = assign (Sum.inl x)

source

@[simp]

theorem Std.Sat.AIG.toCNF.projectRightAssign_property {aig✝ : AIG Nat} {assign : aig✝.CNFVar → Bool} {x : Nat} {hx : x < aig✝.decls.size} :

projectRightAssign assign x hx = assign (Sum.inr ⟨x, hx⟩)

source

def Std.Sat.AIG.toCNF.cnfSatAssignment (aig : 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

Instances For

source

@[simp]

theorem Std.Sat.AIG.toCNF.satAssignment_inl {aig : AIG Nat} {assign1 : Nat → Bool} {x : Nat} :

cnfSatAssignment aig assign1 (Sum.inl x) = assign1 x

source

@[simp]

theorem Std.Sat.AIG.toCNF.satAssignment_inr {aig : AIG Nat} {assign1 : Nat → Bool} {x : Fin aig.decls.size} :

cnfSatAssignment aig assign1 (Sum.inr x) = ⟦assign1, { aig := aig, ref := { gate := ↑x, invert := false, hgate := ⋯ } }⟧

source

def Std.Sat.AIG.toCNF.Cache.Inv {aig : AIG Nat} (cnf : CNF aig.CNFVar) (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 corresponding auxiliary variable as a result.

Equations

Instances For

source

theorem Std.Sat.AIG.toCNF.Cache.Inv_init {aig : AIG Nat} :

Inv [] (Array.replicate aig.decls.size false) ⋯

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

source

structure Std.Sat.AIG.toCNF.Cache (aig : AIG Nat) (cnf : 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 : Inv cnf self.marks ⋯
The invariant to make sure that marks is well formed with respect to the cnf

Instances For

source

structure Std.Sat.AIG.toCNF.Cache.IsExtensionBy {aig : AIG Nat} {cnf1 cnf2 : CNF aig.CNFVar} (cache1 : Cache aig cnf1) (cache2 : 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.

Instances For

source

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

cache1.IsExtensionBy cache3 new1 hnew1

source

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

cache1.IsExtensionBy cache3 new2 hnew2

source

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

cache.IsExtensionBy cache idx ⋯

Cache extension is a reflexive relation.

source

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

cache1.IsExtensionBy cache2 idx ⋯

source

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

Cache aig []

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

Equations

Instances For

source

def Std.Sat.AIG.toCNF.Cache.addFalse {aig : AIG Nat} {cnf : CNF aig.CNFVar} (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.false) :

{ out : Cache aig (Decl.falseToCNF (Sum.inr ⟨idx, h⟩) ++ cnf) // cache.IsExtensionBy out idx h }

Add a Decl.false to a Cache.

Equations

Instances For

source

def Std.Sat.AIG.toCNF.Cache.addAtom {aig : AIG Nat} {cnf : CNF aig.CNFVar} {a : Nat} (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.atom a) :

{ out : Cache aig (Decl.atomToCNF (Sum.inr ⟨idx, h⟩) (Sum.inl a) ++ cnf) // cache.IsExtensionBy out idx h }

Add a Decl.atom to a cache.

Equations

Instances For

source

def Std.Sat.AIG.toCNF.Cache.addGate {aig : AIG Nat} {cnf : CNF aig.CNFVar} {lhs rhs : Fanin} (cache : Cache aig cnf) {hlb : lhs.gate < cache.marks.size} {hrb : rhs.gate < cache.marks.size} (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.gate lhs rhs) (hl : cache.marks[lhs.gate] = true) (hr : cache.marks[rhs.gate] = true) :

{ out : Cache aig (Decl.gateToCNF (Sum.inr ⟨idx, h⟩) (Sum.inr ⟨lhs.gate, ⋯⟩) (Sum.inr ⟨rhs.gate, ⋯⟩) lhs.invert rhs.invert ++ cnf) // cache.IsExtensionBy out idx h }

Add a Decl.gate to a cache.

Equations

Instances For

source

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

Prop

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

Equations

Instances For

source

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

Inv []

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

source

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

Inv (cnf1 ++ cnf2)

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

source

theorem Std.Sat.AIG.toCNF.State.Inv_falseToCNF {upper : Nat} {aig : AIG Nat} {h : upper < aig.decls.size} (heq : aig.decls[upper] = Decl.false) :

Inv (Decl.falseToCNF (Sum.inr ⟨upper, h⟩))

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

source

theorem Std.Sat.AIG.toCNF.State.Inv_atomToCNF {upper : Nat} {aig : AIG Nat} {h : upper < aig.decls.size} {a : Nat} (heq : aig.decls[upper] = Decl.atom a) :

Inv (Decl.atomToCNF (Sum.inr ⟨upper, h⟩) (Sum.inl a))

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

source

theorem Std.Sat.AIG.toCNF.State.Inv_gateToCNF {upper : Nat} {lhs rhs : Fanin} {aig : AIG Nat} {h : upper < aig.decls.size} (heq : aig.decls[upper] = Decl.gate lhs rhs) :

Inv (Decl.gateToCNF (Sum.inr ⟨upper, h⟩) (Sum.inr ⟨lhs.gate, ⋯⟩) (Sum.inr ⟨rhs.gate, ⋯⟩) lhs.invert rhs.invert)

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

source

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

Type

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

cnf : CNF aig.CNFVar
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 self.cnf
The invariant that cnf has to maintain as we build it up.

Instances For

source

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

State aig

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

Equations

Instances For

source

@[reducible, inline]

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

Prop

State extension are Cache.IsExtensionBy for now.

Equations

Instances For

source

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

state1.IsExtensionBy state3 new1 hnew1

source

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

state1.IsExtensionBy state3 new2 hnew2

source

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

state.IsExtensionBy state idx ⋯

State extension is a reflexive relation.

source

def Std.Sat.AIG.toCNF.State.addFalse {aig : AIG Nat} (state : State aig) (idx : Nat) (h : idx < aig.decls.size) (htip : aig.decls[idx] = Decl.false) :

{ out : State aig // state.IsExtensionBy out idx h }

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

Equations

Instances For

source

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

{ out : State aig // state.IsExtensionBy out idx h }

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

Equations

Instances For

source

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

{ out : State aig // state.IsExtensionBy out idx h }

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

Equations

Instances For

source

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

Bool

Evaluate the CNF contained within the state.

Equations

Instances For

source

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

Prop

The CNF within the state is sat.

Equations

Instances For

source

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

Prop

The CNF within the state is unsat.

Equations

Instances For

source

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

Sat assign state ↔ CNF.Sat assign state.cnf

source

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

state.Unsat ↔ state.cnf.Unsat

source

@[simp]

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

eval assign state = CNF.eval assign state.cnf

source

@[simp]

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

Sat assign state ↔ CNF.Sat assign state.cnf

source

@[simp]

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

state.Unsat ↔ state.cnf.Unsat

source

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

CNF Nat

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

Equations

Instances For

source

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

Nat

Equations

Instances For

source

@[irreducible]

def Std.Sat.AIG.toCNF.go (aig : AIG Nat) (upper : Nat) (h : upper < aig.decls.size) (state : State aig) :

{ out : State aig // state.IsExtensionBy out upper h }

Equations

Instances For

source

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

inj a = 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.

source

theorem Std.Sat.AIG.toCNF.go_marks {aig : AIG Nat} {start : Nat} {h : start < aig.decls.size} {state : State aig} :

(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.

source

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

State.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val

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

source

theorem Std.Sat.AIG.toCNF.go_as_denote' (aig : AIG Nat) (start : Nat) (inv : Bool) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) :

⟦assign1, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ = true → State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true

source

theorem Std.Sat.AIG.toCNF.go_as_denote {inv sat? : Bool} (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool) :

(⟦assign1, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ && State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val) = sat? → ⟦assign1, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ = sat?

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

source

theorem Std.Sat.AIG.toCNF.denote_as_go {aig : AIG Nat} {start : Nat} {inv : Bool} {h1 : start < aig.decls.size} {assign : aig.CNFVar → Bool} :

⟦projectLeftAssign assign, { aig := aig, ref := { gate := start, invert := inv, hgate := h1 } }⟧ = false → CNF.eval assign ([(Sum.inr ⟨start, h1⟩, !inv)] :: (go aig start h1 (State.empty aig)).val.cnf) = false

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

source

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

(toCNF entry).Unsat ↔ entry.Unsat

An AIG is unsat iff its CNF is unsat.