As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
The satisfiability (SAT) problem is to find an assignment of binary values to the variables which satisfy a given formula. Many practical application problems can be transformed to SAT problems and many SAT solvers have been developed. In many SAT solvers, preprocessors are widely used to reduce the computational cost. In this paper, we describe an approach for implementing a preprocessor (Unhiding) on FPGA. In the Unhiding, literals and clauses are eliminated to reduce the search space by finding the redundancies in the formula. The data size of the formula is very large in general, and the acceleration is limited by the throughput of the off-chip DRAM banks. In our approach, N clauses are processed in parallel, and the literals in them are sorted into K shift registers so that K banks in the external DRAMs can be accessed in round robin order to achieve higher memory throughout.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.