Abstract
Considerable progress has recently been made in using clause weighting algorithms such as DLM and SDF to solve SAT benchmark problems. While these algorithms have outperformed earlier stochastic techniques on many larger problems, this improvement has been bought at the cost of extra parameters and the complexity of fine tuning these parameters to obtain optimal run-time performance. This paper examines the use of parameters, specifically in relation to DLM, to identify underlying features in clause weighting that can be used to eliminate or predict workable parameter settings. To this end we propose and empirically evaluate a simplified clause weighting algorithm that replaces the tabu list and flat moves parameter used in DLM. From this we show that our simplified clause weighting algorithm is competitive with DLM on the four categories of SAT problem for whichDLMhas already been optimised.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
J. Frank. Learning short term weights for GSAT. In “Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97)”, pages 384–389, 1997.
I. Gent and T. Walsh. Towards an understanding of hill-climbing procedures for SAT. In Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), pages 28–33, 1993.
F. Glover. Tabu search: Part 1. ORSA Journal on Computing, 1(3):190–206, 1989.
B. Mazure, S. Lakhdar, and E. Gregoire.Tabu search forSAT. In Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI-97), pages 281–285, 1997.
P. Morris. The Breakout method for escaping local minima. In Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI-93), pages 40–45, 1993.
D. Schuurmans and F. Southey. Local search characteristics of incomplete SAT procedures. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-00), pages 297–302, 2000.
D. Schuurmans, F. Southey, and R. Holte. The exponentiated subgradient algorithm for heuristic Boolean programming. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), pages 334–341, 2001.
B. Selman and H. Kautz. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI-93), pages 290–295, 1993.
Y. Shang and B. Wah. A discrete Lagrangian-based global search method for solving satisfiability problems. J. Global Optimization, 12:61–99, 1998.
Z. Wu and B. Wah. Trap escaping strategies in discrete Lagrangian methods for solving hard satisfiability and maximum satisfiability problems. In Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI-99), pages 673–678, 1999.
Z. Wu and B. Wah. An efficient global-search strategy in discrete Lagrangian methods for solving hard satisfiability problems. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI-00), pages 310–315, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thornton, J., Pullan, W., Terry, J. (2002). Towards Fewer Parameters for SAT Clause Weighting Algorithms. In: McKay, B., Slaney, J. (eds) AI 2002: Advances in Artificial Intelligence. AI 2002. Lecture Notes in Computer Science(), vol 2557. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36187-1_50
Download citation
DOI: https://doi.org/10.1007/3-540-36187-1_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00197-3
Online ISBN: 978-3-540-36187-9
eBook Packages: Springer Book Archive