A new FPGA-based DPLL algorithm to improve SAT solvers
Résumé
SAT (SATisfiability of Propositional Formula) is a well-known NP-Complete problem [1][2]. Conventional solvers for SAT based on traditional DPLL algorithm presents serious CPU-Times limitations, especially when addressing large size instances. These last decades, a promising approach has emerged for solving efficiently large size instances by using FPGA architectures. This paper follows this last direction and proposes a new and original DPLL solving algorithm based on FPGA. This new FPGA-based DPLL algorithm will use a new backtrack method to reduce the time of problems resolution by using registers which help to save data from the RAM.