Galois Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving
abcBridge: Functional interfaces for AIGs and SAT solving
Edward Z. Yang
SAT solvers are perhaps the most under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NP-complete problems in time for lunch, and there are many, many practical problem domains which involve NP-complete problems. However, a major roadblock to using a SAT solver in your every day routine is translating your problem into SAT, and then running it on a highly optimized SAT solver, which is probably implemented in C or C++ and not your usual favorite programming language.
This talk is about the use, design and implementation of abcBridge, a set of Haskell bindings for ABC, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC looks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs), are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.