|
Change #4032
2010-08-19
15:25:06
|
create
Calagator::Event
1250459142
Galois Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving
Roll back
| description |
nil |
→ |
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 strenght 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. |
| end_time |
nil |
→ |
2010-08-24 11:30:00 -0700 |
| id |
nil |
→ |
1250459142 |
| start_time |
nil |
→ |
2010-08-24 10:30:00 -0700 |
| title |
nil |
→ |
Galois Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving |
| url |
nil |
→ |
http://www.galois.com/blog/2010/08/19/tech-talk-abcbridge-functional-interfaces-for-aigs-and-sat-solving/ |
| venue_id |
nil |
→ |
202390439 |
|