Satisfiability on reconfigurable hardware

Abstract

In this paper we present a new approach to implement satisfiability (SAT) on reconfigurable hardware. Given a combinational circuit C, we automatically design a SAT circuit whose architecture implements a branch-and-bound SAT algorithm specialized for C. A major novel feature is that both the next variable to assign and its value are dynamically determined by a backward model traversal done in hardware. Our approach relies on fine-grain massive parallelism.