Documentation

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.toCNF (entry : Entrypoint Nat) :
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.
Instances For
    source
    theorem Std.Sat.AIG.toCNF_equisat (entry : Entrypoint Nat) :
    (toCNF entry).Unsat ↔ entry.Unsat

    An AIG is unsat iff its CNF is unsat.