leanprover / leansat

This package provides an interface and foundation for verified SAT reasoning
Apache License 2.0
48 stars 6 forks source link

Investigate Local Two-Level And-Inverter Graph Minimization without Blowup #82

Open hargoniX opened 3 months ago

hargoniX commented 3 months ago

https://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf describes a series of optimizations for AIGs that we might be interested in applying. Some of the basic ones are already implemented. We should check whether the remainder is worth it to implement and verify.