Multiagent SAT (MASSAT): Autonomous Pattern Search in Constrained Domains

  • Xiaolong Jin
  • Jiming Liu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2412)


In this paper, we present an autonomous pattern search approach to solving Satisfiability Problems (SATs). Our approach is essentially a multiagent system. To solve a SAT problem, we first divide variables into groups, and represent each variable group with an agent. Then, we randomly place each agent onto a position in the correspoding local space which is composed of the domains of the variables that are represented by this agent. Thereafter, all agents will autonomously make search decisions guided by some reactive rules in their local spaces until a special pattern (i.e., solution) is found or a time step threshold is reached. Experimental results on some benchmark SAT test-sets have shown that by employing the MASSAT approach, we can obtain performances comparable to those of other popular algorithms.


Autonomous Pattern Search Satisfiability Problem (SAT) Multiagent System MASSAT 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    B. J. Bayardo Jr. and R. C. Schrag, Using CSP Look-back Techniques to Solve Real-world SAT Instances, in Proceedings of the 14th National Conference on Artificial Intelligence, pp. 203–208, 1997.Google Scholar
  2. 2.
    J. M. Crawford and L. D. Auton, Experimental Results on the Crossover Point in Random 3SAT, Artificial Intelligence, Vol. 81, No. 1-2, pp. 31–57, 1996.CrossRefMathSciNetGoogle Scholar
  3. 3.
    S.A. Cook, The Complexity of theorem proving procedures, in Proceedings of the 3rd Annual ACM Symposium on the Theory of Computation, pp. 151–158, 1971.Google Scholar
  4. 4.
    J. Gu, Efficient local search for very large-scale satisfiability problem, SIGART Bulletin, vol. 3, pp. 8–12, 1992.CrossRefGoogle Scholar
  5. 5.
    E. A. Hirsch and A. Kojevnikov, UnitWalk: A new SAT solver that uses local search guided by unit clause elimination, in Proceedings of the 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002), pp. 35–42, 2002.Google Scholar
  6. 6.
    H. H. Hoos, On the run-time behavior of stochastic local search algorithms for SAT, in Proceedings of the 16th National Conference on Artificial Intelligence, AAAI’99, pp. 661–666, 1999.Google Scholar
  7. 7.
    C. M. Li and Anbulagan, Look-ahead Versus Look-back for Satisfiability Problems, in Proceedings of CP’97, pp. 341–345, 1997.Google Scholar
  8. 8.
    J. Liu, Autonomous Agents And Multi-Agent Systems: Explorations in Learning, Self-Organization and Adaptive Computation, World Scientific, 2001.Google Scholar
  9. 9.
    J. Liu, H. Jing and Y. Y. Tang, Multi-agent oriented constraint satisfaction Artificial Intelligence, vol. 136, pp. 101–144, 2002.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    J. P. Marques-Silva and K. A. Sakallah, GRASP-A New Search Algorithm for Satisfiability, in Proceedings of IEEE/ACM International Conference on Computer-Aided Design, 1996.Google Scholar
  11. 11.
    B. Mazure, L. Sais, and É. Grégoire, Tabu Search for SAT, in Proceedings of AAAI’97, pp. 281–285, 1997.Google Scholar
  12. 12.
    D. McAllester, B. Selman, and H. Levesque, Evidence for Invariants in Local Search, in Proceedings of AAAI’97, pp. 321–326, 1997.Google Scholar
  13. 13.
    D. Schuurmans and F. Southey, Local search characteristics of incomplete SAT procedures, Artificial Intelligence, vol. 132, no. 2, pp. 121–150, 2001.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    B. Selman, H. A. Kautz, and B. Cohen, Noise Strategies for Improving Local Search, in Proceedings of AAAI’94, pp. 337–343, 1994.Google Scholar
  15. 15.
    B. Selman, H. Levesque, and D. Mitchell, A New Method for Solving Hard Satisfiability Problems, in Proceedings of AAAI’92, pp. 440–446, 1992.Google Scholar
  16. 16.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Xiaolong Jin
    • 1
  • Jiming Liu
    • 1
  1. 1.Department of Computer ScienceHong Kong Baptist UniversityHong Kong

Personalised recommendations