Abstract
In recent years, there has been much research on local search techniques for solving constraint satisfaction problems, including Boolean satisfiability problems. Some of the most successful procedures combine a form of random walk with a greedy bias. These procedures are quite effective in a number of problem domains, for example, constraint-based planning and scheduling, graph coloring, and hard random problem instances. However, in other structured domains, backtrack-style procedures are often more effective. We introduce a technique that leads to significant speedups of random walk style procedures on structured problem domains. Our method identifies long range dependencies among variables in the underlying problem instance. Such dependencies are made explicit by adding new problem constraints. These new constraints can be derived efficiently, and, literally, “accelerate” the Random Walk search process. We provide a formal analysis of our approach and an empirical validation on a recent benchmark collection of hardware verification problems.
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
F. Bacchus and P. van Beek. On the Conversion between Non-Binary and Binary Constraint Satisfaction Problems. In Proceedings of AAAI-98, pages 311–318, 1998.
M. Davis and H. Putnam. A Computing Procedure for Quantification Theory. Journal of the ACM, 7: 201–205, 1960.
M. Davis, G. Logemann, and D. Loveland. A Machine Program for Theorem-Proving. Communications of the ACM, 5:394–397, 1962.
B. Bonet and H. Geffner. Planning as Heuristic Search. Artificial Intelligence, Special issue on Heuristic Search. Vol 129(1–2) 2001.
R. I. Brafman. A Simplifier for Propositional Formulas with Many Binary Clauses, In Proceedings IJCAI-2001, Seattle, WA, pages 515–520, 2001.
B. Cha and K. Iwama. Adding New Clauses for Faster Local Search. In Proceedings AAAI-96, pages 332–337, 1996.
L. Drake, A. Frisch, and T. Walsh. Adding resolution to the DPLL procedure for Satisfiability. In Proceedings of SAT2002, pages 122–129, 2002.
I. Gent and T. Walsh. An Empirical Analysis of Search in GSAT. JAIR, 1993.
C. P. Gomes, B. Selman, N. Crator, and H. Kautz. Heavy-Tailed Phenomenia in Satisfiability and Constraint Satisfication Problems. Journal of Automated Reasoning, Vol 24, No 1–2, February 2000.
J. Gu. Efficient Local Search for Very Large-Scale Satisfiability Problems. SIGART Bulletin 3(1): 8–12, 1992.
E. A. Hirsch and A. Kojevnikov. Solving Boolean Satisfiability Using Local Search Guided by Unit Clause Elimination. In Proc. of CP-2001, 2001.
H. Kautz and B. Selman. Unifying SAT-based and Graph-based Planning. In Proceedings of IJCAI-99, Stockholm, 1999.
J. Kleinberg. Navigation in a small-world. Nature, 406, 2000.
S. Lin and B. W. Kernighan. An Effective Heuristic Algorithm for the Traveling-Salesman Problem. Operations Research, Vol. 21, 2, pages 498–516, 1973.
D. A. McAllester, B. Selman, and H. A. Kautz. Evidence for Invariants in Local Search. In Proceedings of AAAI-97, pages 321–326, 1997.
P. Morris. Breakout method for escaping from local minima. Proc. AAAI-93, Washington, DC (1993).
S. Minton, M. D. Johnson, A. B. Philips, and P. Laird. Solving Large-Scale Constraint Satisfaction and Scheduling Problems Using a Heuristic Repair Methods. Artificial Intelligence 58, pages 161–205, 1990.
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering a Highly Efficient SAT Solver. 38th Design Autom. Conference (DAC 01), 2001.
C. H. Papadimitriou. On Selecting a Satisfying Truth Assignment. In Proceedings of the Conference on the Foundations of Computer Science, pages 163–169, 1991.
A. J. Parkes and J. P. Walser. Tuning Local Search for Satisfiability Testing. In Proc. AAAI-96, 1996.
S. Prestwich. SAT Problems with Chains of Dependent Variables. Unpublished technical note, 2001.
U. Schoening. A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems. In Proceeedings of FOCS, 1999.
D. Schuurmans, F. Southey, and R. C. Holte. The Exponential Subgradient Algorithm for Heuristic Boolean Programming. In Proc. IJCAI-2001, 2001.
B. Selman, H. Kautz, and B. Cohen. Local Search Strategies for Satisfiability Testing. 2nd DIMACS Challenge on Cliques, Coloring and Satisfiability, 1994.
B. Selman, H. Kautz, and D. McAllester. Ten Challenges in Propositional Reasoning and Search. In Proceedings IJCAI-97, 1997.
B. Selman, H. J. Levesque, and D. G. Mitchell. A New Method for Solving Hard Satisfiability Problems. In Proceedings AAAI-92, pages 440–446, 1992.
T. Suyama, M. Yokoo, and A. Nagoya. Solving Satisfiability Problems on FPGAs Using Experimental Unit Propagation. In Proceedings of CP-99, 1999.
M. N. Velev. Benchmark suites SSS-SAT-1.0, SAT-1.0, October 2000. http://www.ece.cmu.edu/~mvelev
M. N. Velev, and R. E. Bryant. Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors. 38th Design Automation Conference (DAC’ 01), June 2001, pp. 226–231.
J. P. Walser, R. Iyer and N. Venkatasubramanyan. An Integer Local Search Method with Application to Capacitated Production Planning. In Proceedings of AAAI-98, Madison, WI, 1998.
T. Walsh. Search in a Small World. In Proceedings of IJCAI-99, 1999.
D. J. Watts and S. Strogatz. Collective dynamics of’ small-world’ networks. Nature, 393, 440–442 (1998).
Z. Wu and B. W. Wah. An Efficient Global-Search Strategy in Discrete Lagrangian Methods for Solving Hard Satisfiability Problems. Proc. AAAI-2000, 2000.
H. Zhang. SATO: An Efficient Propositional Prover. International Conference on Automated Deduction (CADE 97), LNAI 1249, Springer-Verlag, 1997.
Available at http://www.cs.washington.edu/homes/kautz/walksat/
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
Wei, W., Selman, B. (2002). Accelerating Random Walks. In: Van Hentenryck, P. (eds) Principles and Practice of Constraint Programming - CP 2002. CP 2002. Lecture Notes in Computer Science, vol 2470. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46135-3_15
Download citation
DOI: https://doi.org/10.1007/3-540-46135-3_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44120-5
Online ISBN: 978-3-540-46135-7
eBook Packages: Springer Book Archive