Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving

  • Date  Time
  • Speaker
  • Location

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

 

title:
abcBridge: Functional interfaces for AIGs and SAT solving (slides, video)
presenter:
Edward Z. Yang
time:

10:30am, Tuesday, 24 August 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:
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.
bio:
Edward Z. Yang is an undergraduate studying computer science at MIT. He has been interning at Galois over the summer and enjoying every second of it. His interests include blogging, functional programming and practical applications of computer science research. You can read his blog at http://blog.ezyang.com/