Resolvedor modular de satisfabilidade aplicado na verificação de circuitos combinacionais

• Main Author: Bernardo Cunha Vieira
• Other Authors: Antonio Otavio Fernandes
• Format: Others
• Language: Portuguese
• Published: Universidade Federal de Minas Gerais 2010
• Online Access: http://hdl.handle.net/1843/SLSS-85BKJJ

=== The state-of-the-art SAT solvers, as Chaff, zChaff, BerkMin, and Minisat usually share the same core heuristics, for instance: conflict clause recording, non-chronological backtracking and two-watched literals. Nevertheless, they generally differ in the elimination of learnt clauses, as well as in the decision heuristic which selects the next literal. This paper presents a modular CNF-based SAT solver that implements several heuristics such as those proposed by Goldberg and Novikov in BerkMin, and in Equivalence Checking of Dissimilar Circuits, and Niklas Eén and Niklas Srensson in Minisat. The latter solver, which was the starting point for the proposed solver, has been reimplemented to provide a framework in which new heuristics may be tested by a simple description in an XML file, thus easily and rapidly generating new and different SAT solvers. In order to demonstrate the effectiveness of the proposed CNF SAT solver, this paper also proposed five distinct instances of the modular SAT solver for a complex and important SAT solver problem: the Combinational Equivalence Checking problem (CEC). The first instance is a SAT solver that uses BerkMin and Dissimilar Circuits core heuristics except the learnt clause elimination heuristic that had been adapted from Minisat; the second is based on the first and changes between BerkMin and Minisat decision heuristics at run time; the third is based on the first and uses Minisat's decision heuristic; the forth is the implementation of BerkMin and Dissimilar Circuits; the last is yet another SAT solver, based on the first instance, that changes the database reducing heuristic at run time. The experiments demonstrate that the first hypothesis implemented in this modular approach generates a faster solver than state-of-the-art SAT solvers BerkMin and Minisat for several CEC instances. === Os resolvedores SAT atuais, como Chaff, zChaff, BerkMin, e Minisat geralmente compartilham das mesmas heurísticas principais, como por exemplo: aprendizado de cláusulas de conflito, backtracking não cronológico, e a estrutura dos dois literais vigiados. Por outro lado, eles se diferenciam na remoção de cláusulas de conflito, bem como na heurística de decisão do próximo literal. Esta dissertação apresenta uma nova abordagem para a construção de resolvedores SAT. Ela é baseada em fórmulas na forma normal conjuntiva, e implementa diversas heurísticas, como as propostas por Goldberg e Novikov em BerkMin, e em Equivalência de Circuitos Dissimilares, e Niklas Eén and Niklas Srensson no Minisat. O Minisat, que foi o ponto de partida para a abordagem proposta, foi reimplementado para prover um framework no qual novas heurísticas podem ser testadas pela simples descrição em arquivos XML, realmente facilitando e tornando mais rápida a geração de novos e diferentes resolvedores SAT. Para demonstrar a efetividade da abordagem, esta dissertação também propõe cinco instâncias do resolvedor SAT modular para um importante e complexo problema de SAT: o problema da Equivalência de Circuitos Combinacionais. A primeira instância é um resolvedor que utiliza as heurísticas do BerkMin e do artigo Circuitos Dissimilares, menos a de remoção de cláusulas aprendidas, que foi adaptada do Minisat; a segunda instância é uma modificação da primeira que chaveia entre as heurísticas de decisão do BerkMin e do Minisat em tempo de execução; a terceira instância utiliza as heurísticas do BerkMin e do Circuitos Dissimilares menos a de decisão e remoção das cláusulas aprendidas que são adaptadas do Minisat; a quarta instância utiliza todas as heurísticas do BerkMin e do Circuitos Dissimilares; e a última é uma modificação da primeira que chaveia entre as heurísticas de remoção de cláusulas aprendidas em tempo de execução. Os experimentos mostram que a primeira instância gera um resolvedor que é mais rápido que os resolvedores estado-da-arte BerkMin e Minisat para diversas instâncias do problema SAT escolhido.