Hardware Implementations of Real-Time Reconfigurable WSAT Variants
Local search methods such as WSAT have proven to be successful for solving SAT problems. In this paper, we propose two host-FPGA (Field Programmable Gate Array) co-implementations, which use modified WSAT algorithms to solve SAT problems. Our implementations are reconfigurable in real-time for different problem instances. On an XCV1000 FPGA chip, SAT problems up to 100 variables and 220 clauses can be solved. The first implementation is based on a random strategy and achieves one flip per clock cycle through the use of pipelining. The second uses a greedy heuristic at the expense of FPGA space consumption, which precludes pipelining. Both of the two implementations avoid re-synthesis, placement, routing for different SAT problems, and show improved performance over previously published reconfigurable SAT implementations on FPGAs.
KeywordsClock Cycle Field Programmable Gate Array Hardware Implementation FPGA Implementation Stochastic Local Search
Unable to display preview. Download preview PDF.
- 1.Selman, B., Kautz, H., Cohen, B.: Noise strategies for improving local search. In: Proc. National Conference on Artificial Intelligence, pp. 337–343 (1994)Google Scholar
- 2.McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: Proc. 14th National Conference on Artificial Intelligence (AAAI 1997) (1997)Google Scholar
- 3.Hamadi, Y., Merceron, D.: Reconfigurable architectures: A new vision for optimization problems. In: Principles and Practice of Constraint Programming, pp. 209–221 (1997)Google Scholar
- 6.Henz, M., Tan, E., Yap, R.: One flip per clock cycle. In: Proc. of the 7th International Conference on Principles and Practice of Constraint Programming, pp. 509–523 (2001)Google Scholar
- 8.Xilinx. Virtex 2.5 Field programmable gate arrays (1999)Google Scholar
- 10.Zhang, W., Huang, Z., Zhang, J.: Parallel Execution of Stochastic Search, Procedures on Reduced SAT Instances. In: Proc. of the Seventh Pacific Rim International Conference on Artificial Intelligence, pp. 108–117 (2002)Google Scholar
- 11.Kautz, H., Selman, B.: Walksat homepage, http://www.cs.washington.edu/homes/kautz/walksat/