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

Abstract

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.