Abstract
It is well known that the ratio of the number of clauses to the number of variables in a random k-SAT instance is highly correlated with the instance’s empirical hardness. We consider the problem of identifying such features of random SAT instances automatically using machine learning. We describe and analyze models for three SAT solvers – kcnfs, oksolver and satz – and for two different distributions of instances: uniform random 3-SAT with varying ratio of clauses-to-variables, and uniform random 3-SAT with fixed ratio of clauses-to-variables. We show that surprisingly accurate models can be built in all cases. Furthermore, we analyze these models to determine which features are most useful in predicting whether an instance will be hard to solve. Finally we discuss the use of our models to build SATzilla, an algorithm portfolio for SAT.
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
Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341–355. Springer, Heidelberg (2004)
Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the Really Hard Problems Are. In: Proc. IJCAI 1991, pp. 331–337 (1991)
Gomes, C., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. of Automated Reasoning 24(1), 67–100 (2000)
Hoos, H.H., Stützle, T.: Stochastic Local Search – Foundations and Applications. Morgan Kaufmann, San Francisco (2004) (to appear)
Hoos, H.H.: SAT-encodings, search space structure, and local search performance. In: Proc. IJCAI 1999, pp. 296–302. Morgan Kaufmann, San Francisco (1999)
Hoos, H.H., Stützle, T.: Towards a characterisation of the behaviour of stochastic local search algorithms for sat. Artificial Intelligence 112, 213–232 (1999)
Horvitz, E., Ruan, Y., Gomes, C., Kautz, H., Selman, B., Chickering, M.: A Bayesian approach to tackling hard computational problems. In: Proc. UAI 2001, pp. 235–244 (2001)
Kolaitis, P.: Constraint satisfaction, databases and logic. In: Proc. IJCAI 2003, pp. 1587–1595 (2003)
Leyton-Brown, K., Nudelman, E., Andrew, G., McFadden, J., Shoham, Y.: Boosting as a metaphor for algorithm design. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 899–903. Springer, Heidelberg (2003)
Leyton-Brown, K., Nudelman, E., Andrew, G., McFadden, J., Shoham, Y.: A portfolio approach to algorithm selection. In: Proc. IJCAI 2003, pp. 1542–1542 (2003)
Leyton-Brown, K., Nudelman, E., Shoham, Y.: Learning the empirical hardness of optimization problems: The case of combinatorial auctions. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 556–572. Springer, Heidelberg (2002)
Lobjois, L., Lemaître, M.: Branch and bound algorithm selection by performance prediction. In: Proc. AAAI 1998, pp. 353–358 (1998)
Monasson, R., Zecchina, R., Kirkpatrick, S., Selman, B., Troyansky, L.: Determining computational complexity from characteristic ‘phase transitions’. Nature 400, 133–137 (1999)
Ruan, Y., Horvitz, E., Kautz, H.: Restart policies with dependence among runs: A dynamic programming approach. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 573–586. Springer, Heidelberg (2002)
Selman, B., Mitchell, D.G., Levesque, H.J.: Generating hard satisfiability problems. Artificial Intelligence 81(1-2), 17–29 (1996)
Tibshirani, R.: Regression shrinkage and selection via the lasso. J. Royal Statist. Soc B 58(1), 267–288 (1996)
Tompkins, D., Hoos, H.: UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 37–46. Springer, Heidelberg (2005)
Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. IJCAI 2003, pp. 1173–1178 (2003)
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
Nudelman, E., Leyton-Brown, K., Hoos, H.H., Devkar, A., Shoham, Y. (2004). Understanding Random SAT: Beyond the Clauses-to-Variables Ratio. In: Wallace, M. (eds) Principles and Practice of Constraint Programming – CP 2004. CP 2004. Lecture Notes in Computer Science, vol 3258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30201-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-30201-8_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23241-4
Online ISBN: 978-3-540-30201-8
eBook Packages: Springer Book Archive