Skip to main content
SpringerLink
Log in

An algorithm based on tabu search for satisfiability problem

  • Correspondence
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

Abstract

In this paper, a computationally effective algorithm based on tabu search for solving the satisfiability problem (TSSAT) is proposed. Some novel and efficient heuristic strategies for generating candidate neighborhood of the current assignment and selecting variables to be flipped are presented. Especially, the aspiration criterion and tabu list structure of TSSAT are different from those of traditional tabu search. Computational experiments on a class of problem instances show that, TSSAT, in a reasonable amount of computer time, yields better results than Novelty which is currently among the fastest known. Therefore, TSSAT is feasible and effective.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Li Wei, Huang Xiong. The analysis of algorithms for the proposition logic satisfiability.Computer Science, 1999, 26(3): 1–9.

    Google Scholar 

  2. Gent I P, Walsh T. The search for satisfaction. http://dream.dai.ed.ac.uk/group/tw/sat/, 1999.

  3. Davis M, Putnam H. A computing procedure for quantification theory.Journal of the ACM, 1960, 7: 201–215.

    Article  MATH  MathSciNet  Google Scholar 

  4. Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. InProceedings of the 10th National Conference on AI, American Association for Artificial Intelligence, 1992, pp. 440–446.

  5. Gu J. Efficient local search for very large-scale satisfiability problems.SIGART Bulletin, 1992, 3(1): 8–12.

    Article  Google Scholar 

  6. Gent I P, Walsh T. An empirical analysis of search in GSAT.Journal of Artificial Intelligence Research, 1993, 1: 47–59.

    MATH  Google Scholar 

  7. Li Wei, Huang Wenqi. A physic-mathematical method for solving conjunctive normal form satisfiability problem.Science in China (Series A), 1994, 24(11): 1208–1217.

    Google Scholar 

  8. Selman B, Kautz H, Cohen B. Noise strategies for improving local search. InProceedings of the 12th National Conference on AI American Association for Artificial, Intelligence, 1994, pp. 337–343.

  9. Spears W M. Simulated annealing for hard satisfiability problems. In Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, Johnson D S, Trick M A (eds.), 1996, pp. 533–558.DIMA CS Series in Discrete Mathematics and Theoretical Computer Science, Volume 26, American Mathematical Society.

  10. Mazure B, Sais L, Gregoire E. Tabu search for SAT. InProceedings of 14th National Conference on Artificial Intelligence, American Association for Artificial Intelligence, AAAI Press/The MIT Press, 1997, pp. 281–285.

  11. Huang Wenqi, Jin Renchao. The quasi-physical personification algorithm for solving SAT problem-Solar.Science in China (Series E), 1997, 27(2): 179–186.

    Google Scholar 

  12. McAllester D, Selman B, Kautz H. Evidence for invariants in local search. InProceedings of the 14th National Conference on AI American Association for Artificial Intelligence, 1997, pp. 321–327.

  13. Glover F, Laguna M. Tabu Search. Kluwer Academic Publishers, Boston, 1997.

    MATH  Google Scholar 

  14. Holger H Hoos, Thomas Stützle. Towards a characterisation of the behavior of stochastic local search algorithms for SAT.Artificial Intelligence, 1999, 112(1/2): 213–232.

    Article  MATH  MathSciNet  Google Scholar 

  15. Mitchell D, Selman B, Levesque H J. Hard and easy distributions of SAT problems. InProc. AAAI-92, San Jose, CA, 1992, pp. 459–465.

Download references

Author information

Authors and Affiliations

  1. School of Computer, Huazhong University of Science and Technology, 430074, Wuhan, P. R. China

    Huang Wenqi, Zhang Defu & Wang Houxiang

Authors
  1. Huang Wenqi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhang Defu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wang Houxiang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Huang Wenqi.

Additional information

This work was supported by the NKBRSF of China (G1998030600).

HUANG Wenqi is a professor and Ph.D. supervisor of the Huazhong University of Science and Technology. His current research interests include solving NP hard problems by quasiphysics and personification method.

ZHANG Defu received his B.S. degree in computational mathematics in 1996, and his M.S. degree in computational mathematics in 1999, both from Xiangtan University. He is currently a Ph.D. candidate in the School of Computer Science at Huazhong University of Science and Technology. His current research interests lie in empirical algorithms, artificial intelligence and combinatorial optimization.

WANG Houxiang is an associate professor and a Ph.D. candidate in the School of Computer Science at Huazhong University of Science and Technology. His current research interests lie in network, multi-media, algorithm design.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Huang, W., Zhang, D. & Wang, H. An algorithm based on tabu search for satisfiability problem. J. of Comput. Sci. & Technol. 17, 340–346 (2002). https://doi.org/10.1007/BF02947312

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02947312

Keywords

Search

Navigation