Abstract
Identifying CSP variables in SAT encodings of combinatorial problems allows one to incorporate CSP-like variable selection heuristics into SAT solvers. We show that such heuristics turn out to be more powerful than the best performing state-of-the-art variable selection heuristics for SAT. In particular, we define five novel CSP-like variable selection heuristics for Chaff —one of the most modern, powerful and robust SAT solvers— and provide experimental evidence that Chaff augmented with those heuristics outperforms the original Chaff solver one order of magnitude on difficult SAT-encoded problems like random binary CSPs, pigeon hole, and graph coloring.
Research partially supported by project CICYT TIC2001-1577-C03-03 funded by the Ministerio de Ciencia y Tecnología.
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
Ansótegui, C., Béjar, R., Cabiscol, A., Li, C.M., Manyà, F.: Resolution methods for many-valued CNF formulas. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, SAT 2002, Cincinnati, USA, pp. 156–163 (2002)
Ansótegui, C., Larrubia, J., Li, C.M., Manyà, F.: Mv-Satz: A SAT solver for many-valued clausal forms. In: 4th International Conference Journées de L’Informatique Messine, JIM 2003, Metz, France (2003)
Ansótegui, C., Manyà, F., Béjar, R., Gomes, C.: Solving many-valued SAT encodings with local search. In: Proceedings of the Workshop on Probabilistics Approaches in Search, 18th National Conference on Artificial Intelligence, AAAI 2002, Edmonton, Canada, 2002 (2002)
Bayardo, R.J., Schrag, R.C.: Using CSP look-back techniques to solve realworld SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI 1997, Providence, RI, USA, pp. 203–208. AAAI Press, Menlo Park (1997)
Beckert, B., Hähnle, R., Manyà, F.: Transformations between signed and classical clause logic. In: Proceedings, International Symposium on Multiple-Valued Logics, ISMVL 1999, Freiburg, Germany, pp. 248–255. IEEE Press, Los Alamitos (1999)
Beckert, B., Hähnle, R., Manyà, F.: The SAT problem of signed CNF formulas. In: Basin, D., et al. (eds.) Labelled Deduction. Applied Logic Series, vol. 17, pp. 61–82. Kluwer, Dordrecht (2000)
Béjar, R., Cabiscol, A., Fernández, C., Manyà, F., Gomes, C.P.: Capturing structure with satisfiability. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 137–152. Springer, Heidelberg (2001)
Béjar, R., Hähnle, R., Manyà, F.: A modular reduction of regular logic to classical logic. In: Proceedings, 31st International Symposium on Multiple-Valued Logics (ISMVL), Warsaw, Poland, pp. 221–226. IEEE CS Press, Los Alamitos (2001)
Béjar, R., Manyà, F.: A comparison of systematic and local search algorithms for regular CNF formulas. In: Hunter, A., Parsons, S. (eds.) ECSQARU 1999. LNCS (LNAI), vol. 1638, pp. 22–31. Springer, Heidelberg (1999)
Béjar, R., Manyà, F.: Solving the round robin problem using propositional logic. In: Proceedings of the 17th National Conference on Artificial Intelligence, AAAI-2000, Austin, TX, USA, pp. 262–266. AAAI Press, Menlo Park (2000)
Bessière, C., Régin, J.: Refining the basic constraint propagation algorithm. In: Proceedings of IJCAI 2001, pp. 309–315 (2001)
Culberson, J.: Graph coloring page: The flat graph generator (1995), See http://web.cs.ualberta.ca/~joe/Coloring/Generators/flat.html
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960)
Génisson, R., Jégou, P.: Davis and Putnam were already checking forward. In: Proceedings of the 12th European Conference on Artificial Intelligence (ECAI), Budapest, Hungary, pp. 180–184 (1996)
Gent, P.: Arc consistency in SAT. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI), Lyon, France (2002)
Haralick, R., Elliot, G.: Increasing tree search efficiency for constraint satisfaction problems. Artificial Intelligence 14, 263–313 (1980)
Hoos, H.: SATLIB: A collection of SAT tools and data (1999), See http://www.satlib.org
Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.: Balance and filtering in structured satisfiable problems. In: Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI 2001, Seattle/WA, USA, pp. 351–358 (2001)
Kautz, H.A., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI 1996, Portland, OR, USA, pp. 1194–1201. AAAI Press, Menlo Park (1996)
Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI 1997, Nagoya, Japan, pp. 366–371. Morgan Kaufmann, San Francisco (1997)
Li, C.M., Anbulagan: Look-ahead versus look-back for satisfiability problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 341–355. Springer, Heidelberg (1997)
Manyà, F., Béjar, R., Escalada-Imaz, G.: The satisfiability problem in regular CNF-formulas. Soft Computing: A Fusion of Foundations, Methodologies and Applications 2(3), 116–123 (1998)
Marques-Silva, J.P., Guerra, L.: Algorithms for satisfiability in combinational circuits based on backtrack search and recursive learning. In: Proc. of XII Symposium on Integrated Circuits and Systems Design (SBCCI) (1999)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: 39th Design Automation Conference (2001)
Sabin, D., Freuder, E.: Contradicting conventional wisdom in constraint satisfaction. In: Proceedings of ECAI 1994, pp. 125–129 (1994)
Selman, B., Kautz, H.A.: Domain-independent extensions of GSAT: Solving large structured satisfiability problems. In: Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI 1993, Chambery, France, pp. 290–295. Morgan Kaufmann, San Francisco (1993)
Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the 12th National Conference on Artificial Intelligence, AAAI 1994, Seattle, WA, USA, pp. 337–343. AAAI Press, Menlo Park (1994)
Selman, B., Levesque, H., Mitchell, D.: A new method for solving hard satisfiability problems. In: Proceedings of the 10th National Conference on Artificial Intelligence, AAAI 1992, San Jose, CA, USA, pp. 440–446. AAAI Press, Menlo Park (1992)
Silva, J.P.M., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)
Smith, B., Dyer, M.: Locating the phase transition in binary constraint satisfaction problems. Artificial Intelligence 81, 155–181 (1996)
Velev, M., Bryant, R.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors. In: 38th Design Automation Conference (DAC 2001) (2001)
Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, p. 441. Springer, Heidelberg (2000)
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
Ansótegui, C., Larrubia, J., Manyà, F. (2003). Boosting Chaff’s Performance by Incorporating CSP Heuristics. In: Rossi, F. (eds) Principles and Practice of Constraint Programming – CP 2003. CP 2003. Lecture Notes in Computer Science, vol 2833. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45193-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-45193-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20202-8
Online ISBN: 978-3-540-45193-8
eBook Packages: Springer Book Archive