Abstract
Considerable progress has recently been made in using clause weighting algorithms to solve SAT benchmark problems. While these algorithms have outperformed earlier stochastic techniques on many larger problems, this improvement has generally required extra, problem specific, parameters which have to be fine tuned to problem domains to obtain optimal run-time performance. In a previous paper, the use of parameters, specifically in relation to the DLM clause weighting algorithm, was examined to identify underlying features in clause weighting that could be used to eliminate or predict workable parameter settings. A simplified clause weighting algorithm (Maxage), based on DLM, was proposed that reduced the parameters to a single parameter. Also, in a previous paper, the structure of SAT problems was investigated and a measure developed which allowed the classification of SAT problems into random, loosely structured or compactly structured. This paper extends this work by investigating the behaviour of Maxage with regard to the structural characteristics of SAT problems. The underlying motivation for this study is the development of an adaptive, parameterless clause weighting algorithm.
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
Frank, J.: Learning short term weights for GSAT. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence (AAAI 1997), pp. 384–389 (1997)
Glover, F.: Tabu search: Part 1. ORSA Journal on Computing 1(3), 190–206 (1989)
Hutter, F., Tompkins, D.A.D., Hoos, H.H.: Scaling and probabilistic smoothing: Efficient dynamic local search for SAT. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 233–248. Springer, Heidelberg (2002)
Kravchuk, O., Pullan, W., Thornton, J., Sattar, A.: An investigation of variable relationships in 3-SAT problems. In: AI 2002: Advances in Artificial Intelligence, pp. 579–590 (2002)
Morris, P.: The Breakout method for escaping local minima. In: Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI 1993), pp. 40–45 (1993)
Schuurmans, D., Southey, F.: Local search characteristics of incomplete SAT procedures. In: Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI 2000), pp. 297–302 (2000)
Schuurmans, D., Southey, F., Holte, R.C.: The exponentiated subgradient algorithm for heuristic boolean programming. In: Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 334–341 (2001)
Selman, B., Kautz, H.: Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In: Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence (IJCAI 1993), pp. 290–295 (1993)
Shang, Y., Wah, B.: A discrete Lagrangian-based global search method for solving satisfiability problems. J. Global Optimization 12, 61–99 (1998)
Thornton, J., Pullan, W., Terry, J.: Towards fewer parameters for SAT clause weighting algorithms. In: AI 2002: Advances in Artificial Intelligence, pp. 569– 578 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pullan, W., Zhao, L., Thornton, J. (2003). Estimating Problem Metrics for SAT Clause Weighting Local Search. In: Gedeon, T.(.D., Fung, L.C.C. (eds) AI 2003: Advances in Artificial Intelligence. AI 2003. Lecture Notes in Computer Science(), vol 2903. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24581-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-24581-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20646-0
Online ISBN: 978-3-540-24581-0
eBook Packages: Springer Book Archive