{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T16:10:25Z","timestamp":1739981425018,"version":"3.37.3"},"reference-count":0,"publisher":"IOS Press","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.3233\/978-1-61499-621-7-515","type":"book-chapter","created":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T15:30:51Z","timestamp":1739979051000},"source":"Crossref","is-referenced-by-count":0,"title":["FPGA Acceleration of SAT Preprocessor"],"prefix":"10.3233","author":[{"family":"Suzuki Masayuki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Maruyama Tsutomu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"7437","container-title":["Advances in Parallel Computing","Parallel Computing: On the Road to Exascale"],"original-title":[],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T15:52:23Z","timestamp":1739980343000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.medra.org\/servlet\/aliasResolver?alias=iospressISBN&isbn=978-1-61499-620-0&spage=515&doi=10.3233\/978-1-61499-621-7-515"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/978-1-61499-621-7-515","relation":{},"ISSN":["0927-5452"],"issn-type":[{"value":"0927-5452","type":"print"}],"subject":[],"published":{"date-parts":[[2016]]}}}