Multiagent SAT (MASSAT): Autonomous Pattern Search in Constrained Domains
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.
KeywordsAutonomous Pattern Search Satisfiability Problem (SAT) Multiagent System MASSAT
Unable to display preview. Download preview PDF.
- 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
- 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
- 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.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.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.J. Liu, Autonomous Agents And Multi-Agent Systems: Explorations in Learning, Self-Organization and Adaptive Computation, World Scientific, 2001.Google Scholar
- 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.B. Mazure, L. Sais, and É. Grégoire, Tabu Search for SAT, in Proceedings of AAAI’97, pp. 281–285, 1997.Google Scholar
- 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
- 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.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