Hardware based algorithm for conflict diagnosis in SAT solver

The Boolean satisfiability problem (SAT) is an NP-complete problem so software SAT´s solving algorithm execution time influences the performance of SAT- based CAD tools. In this paper, we present a new approach for implementing conflict analysis based on a conflicting variables accumulator and priority encoder to determine backtrack level Using this approach, we implement an FPGA-based SAT solver performing depth- first search with conflict directed nonchronological backtracking. We compare our SAT solver with other SAT solvers through instances from DIMACS benchmarks suite.