×

zbMATH — the first resource for mathematics

Local search characteristics of incomplete SAT procedures. (English) Zbl 0983.68180
Summary: Effective local search methods for finding satisfying assignments of CNF formulae exhibit several systematic characteristics in their search. We identify a series of measurable characteristics of local search behavior that are predictive of problem solving efficiency. These measures are shown to be useful for diagnosing inefficiencies in given search procedures, tuning parameters, and predicting the value of innovations to existing strategies. We then introduce a new local search method, SDF (“Smoothed Descent and Flood”), that builds upon the intuitions gained by our study. SDF works by greedily descending in an informative objective (that considers how strongly clauses are satisfied, in addition to counting the number of unsatisfied clauses) and, once trapped in a local minima, “floods” this minima by re-weighting unsatisfied clauses to create a new descent direction. The resulting procedure exhibits superior local search characteristics under our measures. We show that this method can compete with the state of the art techniques, and significantly reduces the number of search steps relative to many recent methods.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68P10 Searching and sorting
68Q25 Analysis of algorithms and problem complexity
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Achlioptas, D.; Gomes, C.; Kautz, H.; Selman, B., Generating satisfiable problem instances, (), 256-261
[2] Bayardo, R.; Schrag, R., Using CSP look-back techniques to solve real-world SAT instances, (), 203-208
[3] Cha, B.; Iwama, K., Performance test of local search algorithms using new types of random CNF formulas, (), 304-310
[4] Cha, B.; Iwama, K., Adding new clauses for faster local search, (), 332-337
[5] Frank, J., Weighting for godot: learning heuristics for GSAT, (), 338-343
[6] Frank, J., Learning short-term weights for GSAT, (), 384-391
[7] Gent, I.; Walsh, T., Towards an understanding of Hill-climbing procedures for SAT, (), 28-33
[8] Gent, I.; Walsh, T., Unsatisfied variables in local search, () · Zbl 0900.68178
[9] Gomes, C.; Selman, B.; Kautz, H., Boosting combinatorial search through randomization, (), 431-437
[10] Gomes, C.; Selman, B.; Kautz, H., Heavy-tailed phenomena in satisfiability and constraint satisfaction problems, J. automat. reason., 24, 1, 67-100, (2000) · Zbl 0967.68145
[11] Hoos, H., On the run-time behavior of stochastic local search algorithms for SAT, (), 661-666
[12] Kautz, H.; Selman, B., Pushing the envelope: planning, propositional logic, and stochastic search, (), 1194-1201
[13] Larrabee, T., Test pattern generation using Boolean satisfiability, IEEE trans. computer-aided design, 11, 1, 4-15, (1992)
[14] Li, C.; Anbulagan, Heuristics based on unit propagation for satisfiability problems, (), 366-371
[15] Mazure, B.; Saı̈s, L.; Grégoire, É., Tabu search for SAT, (), 281-285
[16] McAllester, D.; Selman, B.; Kautz, H., Evidence for invariants in local search, (), 321-326
[17] Morris, P., The breakout method for escaping from local minima, (), 40-45
[18] Parkes, A.; Walser, J., Tuning local search for satisfiability testing, (), 356-362
[19] Ross, S., Introduction to probability models, (1997), Academic Press San Diego · Zbl 0914.60005
[20] Schuurmans, D.; Southey, F., Local search characteristics of incomplete SAT procedures, (), 297-302 · Zbl 0983.68180
[21] Selman, B.; Kautz, H., Domain-independent extensions to GSAT: solving large structured satisfiability problems, ()
[22] Selman, B.; Kautz, H.; Cohen, B., Noise strategies for improving local search, (), 337-343
[23] Selman, B.; Kautz, H.; McAllester, D., Ten challenges in propositional reasoning and search, (), 50-54
[24] Selman, B.; Levesque, H.; Mitchell, D., A new method for solving hard satisfiability problems, (), 440-446
[25] Shang, Y.; Wah, W., A discrete Lagrangian based global search method for solving satisfiability problems, J. global optimization, 12, 1, 61-99, (1998) · Zbl 0904.90154
[26] Wu, Z.; Wah, W., Trap escaping strategies in discrete Lagrangian methods for solving hard satisfiability and maximum satisfiability problems, (), 673-678
[27] Wu, Z.; Wah, W., An efficient global-search strategy in discrete Lagrangian methods for solving hard satisfiability problems, (), 310-315
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.