A Hardware SAT Solver Using Non-chronological Backtracking and Clause Recording Without Overheads

摘要

Boolean satisability (SAT), known as an NP-complete problem, has many important applications. The current generation of software SAT solvers implement non-chronological backtracking and clause recording to improve their performance. However, most hardware SAT solvers do not implement these methods since the methods require a complex process to work. To hasten the solving process compared with a contemporary software SAT solver, hardware SAT solvers need to implement these methods. In this paper, we show a method for implementing these methods without a complex process and design a hardware SAT solver using this method. The experimental results indicate that it is possible to estimate a 24-80x speed increase compared with a contemporary software SAT solver in EDA problems based on a reasonable assumption.