Abstract
Considerable progress in local search has recently been made in using clause weighting algorithms to solve satisfiability benchmark problems. While these algorithms have outperformed earlier stochastic techniques on many larger problems, this improvement has generally required extra, problem specific, parameters requiring fine tuning to problem domains for 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 DLM’s run-time parameters to a single parameter. This paper presents an algorithm, RLS, based on DLM and Maxage, which combines the use of resolvent clauses with clause weighting. In RLS, clause resolvents that contain fewer literals than their parent clauses become active in the SAT problem whenever a parent clause is false and a clause weight increase is performed. This technique reduces the overhead of resolvent clauses and also adds extra information for the local search when it is required. In this paper RLS is compared with the state of the art DLM and SAPS clause weighting local search algorithms.
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
Cha, B., Iwama, K.: Adding new clauses for faster local search. In: Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI 1996), pp. 332–337 (1996)
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)
Hoos, H.H., Stutzle, T.: Towards a characterisation of the behaviour of stochastic local search algorithms for sat. Artificial Intelligence Journal 112, 213–232 (1999)
Hutter, F., Tompkins, 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)
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)
Pullan, W., Zhao, L., Thornton, J.: Estimating problem metrics for sat clause weighting local search. In: Gedeon, T(T.) D., Fung, L.C.C. (eds.) AI 2003. LNCS (LNAI), vol. 2903, pp. 137–149. Springer, Heidelberg (2003)
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)
Wu, Z., Wah, B.: 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 2000), pp. 310–315 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pullan, W., Zhao, L. (2004). Resolvent Clause Weighting Local Search. In: Tawfik, A.Y., Goodwin, S.D. (eds) Advances in Artificial Intelligence. Canadian AI 2004. Lecture Notes in Computer Science(), vol 3060. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24840-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-24840-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22004-6
Online ISBN: 978-3-540-24840-8
eBook Packages: Springer Book Archive