Skip to main content
SpringerLink
Log in

Full Dynamic Substitutability by SAT Encoding

  • Conference paper
Principles and Practice of Constraint Programming – CP 2004 (CP 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3258))

Abstract

Symmetry in constraint problems can be exploited to greatly improve search performance. A form of symmetry that has been the subject of considerable research is value interchangeability. Automatically detecting full interchangeability is thought to be intractable, so research has focused on either discovery of local interchangeability or programmer knowledge of full interchangeability. This paper shows that full dynamic substitutability can be broken in a CSP by reformulating it as a SAT problem. No analysis is necessary, space requirements are modest, solutions are collected into Cartesian products, and unit propagation enforces forward checking on the CSP. In experiments on unsatisfiable problems, better results are obtained than with standard SAT encodings.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bacchus, F., van Beek, P.: On the Conversion Between Non-Binary and Binary Constraint Satisfaction Problems Using the Hidden Variable Method. In: Fifteenth National Conference on Artificial Intelligence, Madison, Wisconsin, USA, pp. 311–318 (1998)

    Google Scholar 

  2. Backofen, R., Will, S.: Excluding Symmetries in Constraint-Based Search. In: Jaffar, J. (ed.) CP 1999. LNCS, vol. 1713, pp. 73–87. Springer, Heidelberg (1999)

    Google Scholar 

  3. Beckwith, A.M., Choueiry, B.Y., Zou, H.: How the Level of Interchangeability Embedded in a Finite Constraint Satisfaction Problem Affects the Performance of Search. In: Stumptner, M., Corbett, D.R., Brooks, M. (eds.) Canadian AI 2001. LNCS (LNAI), vol. 2256, pp. 50–61. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Bellicha, A., Habib, M., Vilarem, M.C., Capelle, C., Kokeny, T.: CSP Techniques Using Partial Orders on Domain Values. In: Schiex, T., Bessière, C. (eds.) ECAI 1994 Workshop on Constraint Satisfaction Issues raised by Practical Applications, Amsterdam (1994)

    Google Scholar 

  5. Benhamou, B.: Study of Symmetry in Constraint Satisfaction Problems. Principles and Practice of Constraint Programming (1994)

    Google Scholar 

  6. Benson, B.W., Freuder, E.C.: Interchangeability Preprocessing Can Improve Forward Checking. In: Tenth European Conference on Artificial Intelligence, Vienna, Austria, pp. 28–30 (1992)

    Google Scholar 

  7. Bèssiere, C., Hebrard, E., Walsh, T.: Local Consistencies in SAT. In: Sixth International Conference on Theory and Applications of Satisfiability Testing, Santa Margherita Ligure, Italy, pp. 400–407 (2003)

    Google Scholar 

  8. Bistarelli, S., Faltings, B.V., Neagu, N.: Interchangeability in Soft CSPs. In: O’Sullivan, B. (ed.) CologNet 2002. LNCS (LNAI), vol. 2627, pp. 31–46. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  9. Bowen, J., Likitvivatanavong, C.: Splitting the Atom: a New Approach to Neighbourhood Interchangeability in Constraint Satisfaction Problems. In: Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico (2003) (poster)

    Google Scholar 

  10. Brglez, F., Li, X.Y., Stallman, M.F.: The Role of a Skeptic Agent in Testing and Benchmarking of SAT Algorithms. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing, University of Cincinnati, pp. 354–361 (2002)

    Google Scholar 

  11. Chmeiss, A., Saïs, L.: About Neighborhood Substitutability in CSPs. In: Third International Workshop on Symmetry in Constraint Satisfaction Problems, Kinsale, Ireland, pp. 41–45 (2003)

    Google Scholar 

  12. Choueiry, B.Y., Davis, A.M.: Dynamic Bundling: Less Effort for More Solutions. In: Koenig, S., Holte, R.C. (eds.) SARA 2002. LNCS (LNAI), vol. 2371, pp. 64–82. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Choueiry, B.Y., Noubir, G.: On the Computation of Local Interchangeability in Discrete Constraint Satisfaction Problems. In: Fifteenth National Conference on Artificial Intelligence, Madison, WI, USA, pp. 326–333 (1998)

    Google Scholar 

  14. Fahle, T., Schamberger, S., Sellman, M.: Symmetry Breaking. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 93–107. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. Freuder, E.C.: Eliminating Interchangeable Values in Constraint Satisfaction Problems. In: Ninth National Conference on Artificial Intelligence, Anaheim, CA, pp. 227–233 (1991)

    Google Scholar 

  16. Gent, I.P.: Arc Consistency in SAT. In: Fifteenth European Conference on Artificial Intelligence, Lyons, France, pp. 121–125 (2002)

    Google Scholar 

  17. Gent, I.P., Harvey, W., Kelsey, T.: Groups and Constraints: Symmetry Breaking During Search. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 415–430. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Gent, I.P., Smith, B.: Symmetry Breaking During Search in Constraint Programming. In: Fourteenth European Conference on Artificial Intelligence, pp. 599–603 (2000)

    Google Scholar 

  19. Haselböck, A.: Exploiting Interchangeabilities in Constraint Satisfaction Problems. In: Thirteenth International Joint Conference on Artificial Intelligence, Chambéry, France, pp. 282–287 (1993)

    Google Scholar 

  20. van Hentenryck, P., Ågren, M., Flener, P., Pearson, J.: Tractable Symmetry Breaking for CSPs with Interchangeable Values. In: Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 2003, pp. 277–282 (2003)

    Google Scholar 

  21. Hubbe, P.D., Freuder, E.C.: An Efficient Cross Product Representation of the Constraint Satisfaction Problem Search Space. In: Tenth National Conference on Artificial Intelligence, San Jose, California, USA, pp. 421–427 (1992)

    Google Scholar 

  22. Lal, A., Choueiry, B.Y., Freuder, E.C.: Neighborhood Interchangeability and Dynamic Bundling for Non-Binary Finite CSPs. In: Joint Annual Workshop of ERCIM / CoLogNet on Constraint Solving and Constraint Logic Programming, Lausanne, Switzerland (2004) (to appear)

    Google Scholar 

  23. Lesaint, D.: Maximal Sets of Solutions for Constraint Satisfaction Problems. In: Eleventh European Conference on Artificial Intelligence, Amsterdam, The Netherlands, pp. 110–114 (1994)

    Google Scholar 

  24. Meseguer, P., Torras, C.: Exploiting Symmetries Within Constraint Satisfaction Search. Artificial Intelligence 129(1-2), 133–163 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  25. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Thirty Eighth Design Automation Conference, Las Vegas, pp. 530–535 (2001)

    Google Scholar 

  26. Parkes, A.J.: Exploiting Solution Clusters for Coarse-Grained Distributed Search. In: IJCAI 2001 Workshop on Distributed Constraint Reasoning, Seattle, Washington, USA (2001)

    Google Scholar 

  27. Prestwich, S.D.: Full Dynamic Interchangeability with Forward Checking and Arc Consistency. In: ECAI 2004 Workshop on Modeling and Solving Problems With Constraints, Valencia, Spain (2004)

    Google Scholar 

  28. Puget, J.-F.: On the Satisfiability of Symmetrical Constrained Satisfaction Problems. In: Komorowski, J., Raś, Z.W. (eds.) ISMIS 1993. LNCS, vol. 689, pp. 350–361. Springer, Heidelberg (1993)

    Google Scholar 

  29. Roney-Dougal, C.M., Gent, I.P., Kelsey, T.W., Linton, S.A.: Tractable Symmetry Breaking using Restricted Search Trees. In: Sixteenth European Conference on Artificial Intelligence, Valencia, Spain (2004) (to appear)

    Google Scholar 

  30. Rossi, F., Petrie, C., Dhar, V.: On the Equivalence of Constraint Satisfaction Problems. In: Nineteenth European Conference on Artificial Intelligence, Stockholm, Sweden, pp. 550–556 (1990)

    Google Scholar 

  31. Silaghi, M.-C., Sam-Haroud, D., Faltings, B.V.: Ways of Maintaining Arc Consistency in Search Using the Cartesian Representation. In: Apt, K.R., Kakas, A.C., Monfroy, E., Rossi, F. (eds.) Compulog Net WS 1999. LNCS (LNAI), vol. 1865, pp. 173–187. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  32. Thiffault, C., Bacchus, F., Walsh, T.: Solving Non-Clausal Formulas with DPLL Search. In: Seventh International Conference on Theory and Applications of Satisfiability Testing, Vancouver, Canada, pp. 147–156 (2004)

    Google Scholar 

  33. Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 441–456. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  34. Weigel, R., Faltings, B.V., Choueiry, B.Y.: Context in Discrete Constraint Satisfaction Problems. In: Twelfth European Conference on Artificial Intelligence, Budapest, Hungary, pp. 205–209 (1996)

    Google Scholar 

  35. Weigel, R., Bliek, C., Faltings, B.V.: On Reformulation of Constraint Satisfaction Problems. In: Thirteenth European Conference on Artificial Intelligence, Brighton, United Kingdom, pp. 254–258 (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cork Constraint Computation Centre, Department of Computer Science, University College, Cork, Ireland

    Steven Prestwich

Authors
  1. Steven Prestwich
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Clayton School of IT, Monash University, Australia

    Mark Wallace

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Prestwich, S. (2004). Full Dynamic Substitutability by SAT Encoding. 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_38

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30201-8_38

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23241-4

  • Online ISBN: 978-3-540-30201-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation