Hardware Implementations of Real-Time Reconfigurable WSAT Variants

  • Roland H. C. Yap
  • Stella Z. Q. Wang
  • Martin J. Henz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2778)


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.


Clock Cycle Field Programmable Gate Array Hardware Implementation FPGA Implementation Stochastic Local Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 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
  4. 4.
    Yung, W.H., Seung, Y.W., Lee, K.H., Leong, P.H.W.: A runtime reconfigurable implementation of the GSAT algorithm. In: Lysaght, P., Irvine, J., Hartenstein, R.W. (eds.) FPL 1999. LNCS, vol. 1673, pp. 526–531. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Leong, P.H.W., Sham, C.W., Wong, W.C., Wong, H.Y., Yuen, W.S., Leong, M.P.: A bistream reconfigurable FPGA implementation of the WSAT algorithm. IEEE Trans. on Very Large Scale Integration (VLSI) Systems 9(1), 197–200 (2001)CrossRefGoogle Scholar
  6. 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
  7. 7.
    Abramovici, M., Sousa, A.: A SAT solver using reconfigurable hardware and virtual logic. Journal of Automated Reasoning 24(1/2), 5–36 (2000)CrossRefGoogle Scholar
  8. 8.
    Xilinx. Virtex 2.5 Field programmable gate arrays (1999)Google Scholar
  9. 9.
    Hoos, H., Stützle, T.: Local search algorithms for SAT: An empirical evaluation. Journal of Automated Reasoning 24, 421–481 (2000)CrossRefGoogle Scholar
  10. 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. 11.
    Kautz, H., Selman, B.: Walksat homepage,

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Roland H. C. Yap
    • 1
  • Stella Z. Q. Wang
    • 1
  • Martin J. Henz
    • 1
  1. 1.School of ComputingNational University of SingaporeSingapore

Personalised recommendations