Utilização de hardware reconfigurável para acelerar a satisfação booleana

• Author(s): Iouliia Skliarova ; António B. Ferrari
• Date: 2012
• Origin: Electrónica e Telecomunicações
• Subject(s): SAT; satisfação booleana; CAD; hardware reconfigurável; SAT; satisfação booleana; CAD; hardware reconfigurável
• Document Type: Article
• Language: Portuguese

Description

The paper presents a case study of accelerating Boolean satisfiability in reconfigurable hardware. Boolean satisfiability (SAT) is an important problem having many applications in CAD and other areas. We propose an application-specific approach to accelerate the backtrack search algorithm for the SAT problem formulated over discrete matrix. The algorithm employed involves a quite sophisticated control unit, which is entirely implemented in reconfigurable hardware. Finally, we analyze different possibilities of solving the SAT problem and argue that the best results can be achieved by the use of software, runningon a general-purpose computer, together with an FPGAbasedreconfigurable SAT solver. Este artigo apresenta um estudo de possibilidade de aceleração da satisfação booleana com a ajuda do hardware reconfigurável. A satisfação booleana (SAT) é um problema importante que tem muitas aplicações em CAD e outras áreas. Neste artigo propomos uma técnica de desenvolvimento orientada a problema em geral para acelerar a resolução de SAT formulado sobre matriz discreta. O algoritmo utilizado requer uma unidade de controlo bastante complexa que é implementada inteiramente em hardware reconfigurável. Por fim, são analisadas diferentes possibilidades de resolução de SAT e argumenta-se que os melhores resultados podem ser obtidos com a ajuda da colaboração de uma aplicação de software executada num computador de uso geral com um circuito de solução de SAT implementado em FPGA.