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.
Produce a Tseitin style CNF for a Decl.gate, using output as the tree node variable.
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
- Std.Sat.AIG.toCNF.mixAssigns assign1 assign2 (Sum.inl var) = assign1 var
- Std.Sat.AIG.toCNF.mixAssigns assign1 assign2 (Sum.inr var) = assign2 var
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 := ⋯ } }⟧
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] = 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 : CNF.eval assign cnf = true) (idx : Nat) (hbound : idx < aig.decls.size) (_hmark : marks[idx] = true) : ⟦projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ = 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.
The CNF cache. It keeps track of AIG nodes that we already turned into CNF to avoid adding the same CNF twice.
Keeps track of AIG nodes that we already turned into CNF.
There are always as many marks as AIG nodes.
We say that a cache extends another by an index when it doesn't invalidate any entry and has an entry for that index.
Add a Decl.atom to a cache.
Add a Decl.gate to a cache.
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
State.Inv holds for the CNF that we produce for a Decl.gate
The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.
The CNF clauses so far.
A cache so that we don't generate CNF for an AIG node more than once.
The invariant that
cnfhas to maintain as we build it up.
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 := ⋯ }
State extension are Cache.IsExtensionBy for now.
Equations
- state1.IsExtensionBy state2 new hnew = state1.cache.IsExtensionBy state2.cache new hnew
Add the CNF for a Decl.gate to the state.
Equations
- One or more equations did not get rendered due to their size.
Evaluate the CNF contained within the state.
Equations
- Std.Sat.AIG.toCNF.State.eval assign state = Std.Sat.CNF.eval assign state.cnf
The CNF within the state is sat.
Equations
- Std.Sat.AIG.toCNF.State.Sat assign state = Std.Sat.CNF.Sat assign state.cnf
Convert an AIG into CNF, starting at some entry node.
Equations
- One or more equations did not get rendered due to their size.
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
Connect SAT results about the CNF to SAT results about the AIG.
An AIG is unsat iff its CNF is unsat.