Skip to main content
SpringerLink
Log in

Learning General Constraints in CSP

  • Conference paper
  • First Online:
Book cover Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9075))

Abstract

We present a new learning scheme for CSP solvers, which is based on learning (general) constraints rather than generalized no-goods or signed-clauses that were used in the past. The new scheme is integrated in a conflict-analysis algorithm reminiscent of a modern systematic SAT solver: it traverses backwards the conflict graph and gradually builds an asserting conflict constraint. This construction is based on new inference rules that are tailored for various pairs of constraints types, e.g., \(x \le y_1 + k_1\) and \(x \ge y_2+ k_2\), or \(y_{1}\le x\) and \([x,y_{2}]\not \subseteq [a,b]\). The learned constraint is stronger than what can be learned via signed resolution. Our experiments show that our solver HCSP backtracks orders of magnitude less than other state-of-the-art solvers, and is overall on par with the winner of this year’s MiniZinc challenge.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. The HCSP Constraint Solver web page. http://tx.technion.ac.il/mveksler/HCSP/

  2. Fourth international CSP solver competition (2009). http://cpai.ucc.ie/09/index.html

  3. Minizinc challenge (2014). http://www.minizinc.org/challenge2014/

  4. Opturion CPX - tool description (2014). http://www.minizinc.org/challenge2014/description_opturion_cpx.txt

  5. Beckert, B., Hähnle, R., Manyá, F.: The SAT problem of signed CNF formulas, pp. 59–80 (2000)

    Google Scholar 

  6. Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press (2009)

    Google Scholar 

  7. Boussemart, F., Hemery, F., Lecoutre, C., Sais, L.: Boosting systematic search by weighting constraints. In: López de Mántaras, R., Saitta, L. (eds.) ECAI, pp. 146–150. IOS Press (2004)

    Google Scholar 

  8. Choi, C.W., Harvey, W., Lee, J.H.M., Stuckey, P.J.: Finite domain bounds consistency revisited. In: Sattar, A., Kang, B.-H. (eds.) AI 2006. LNCS (LNAI), vol. 4304, pp. 49–58. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Dechter, R.: Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artif. Intell. 41(3), 273–312 (1990)

    Article  MathSciNet  Google Scholar 

  11. Dixon, H.E., Ginsberg, M.L.: Inference methods for a pseudo-boolean satisfiability solver. In: Dechter, R., Sutton, R.S. (eds.) Proceedings of the Eighteenth National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence, July 28 - August 1, 2002, Edmonton, Alberta, Canada, pp. 635–640. AAAI Press / The MIT Press (2002)

    Google Scholar 

  12. Feydy, T., Stuckey, P.J.: Lazy clause generation reengineered. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 352–366. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Fujiwara, T.: iZplus - tool description (2014). http://www.minizinc.org/challenge2014/description_izplus.txt

  14. Gent, I.P., Miguel, I., Moore, N.C.A.: Lazy explanations for constraint propagators. In: Carro, M., Peña, R. (eds.) PADL 2010. LNCS, vol. 5937, pp. 217–233. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Stuckey, P.J., Chu, G.: Structure based extended resolution for constraint programming. http://arxiv.org/abs/1306.4418

  16. Hebrard, E.: Mistral, a constraints satisfiaction library. In: Third international CSP solver competition, pp. 31–40 (2008)

    Google Scholar 

  17. Jain, S., Sabharwal, A., Sellmann, M.: A general nogoodlearning framework for pseudo-boolean multi-valued SAT. In: Burgard, W., Roth, D. (eds.) Proceedings of the Twenty-Fifth AAAI Conference on Articial Intelligence, AAAI 2011, San Francisco, California, USA, August 7–11, 2011. AAAI Press (2011)

    Google Scholar 

  18. Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reasoning 51(1), 79–108 (2013)

    Article  Google Scholar 

  19. Katsirelos, G., Bacchus, F.: Unrestricted nogood recording in CSP search. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 873–877. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Katsirelos, G., Bacchus, F.: Generalized nogoods in CSPs. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 390–396. AAAI Press / The MIT Press (2005)

    Google Scholar 

  21. Liu, C., Kuehlmann, A., Moskewicz, M.W.: CAMA: a multi-valued satisfiability solver. In: ICCAD, pp. 326–333. IEEE Computer Society / ACM (2003)

    Google Scholar 

  22. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. Design Automation Conference (DAC 2001) (2001)

    Google Scholar 

  23. Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.R.: MiniZinc: towards a Standard CP Modelling Language. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529–543. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Nieuwenhuis, R.: The IntSat method for integer linear programming. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 574–589. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  25. Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357–391 (2009)

    Article  MathSciNet  Google Scholar 

  26. Strichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Veksler, M., Strichman, O.: A proof-producing CSP solver. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (2010)

    Google Scholar 

  28. Veksler, M., Strichman, O.: A proof-producing CSP solver (a proof supplement). Technical Report IE/IS-2010-02, Industrial Engineering, Technion, Haifa, Israel, January 2010. Available also from [1]

    Google Scholar 

  29. Veksler, M., Strichman, O.: Learning non-clausal constraints in csp (long version). Technical report, Technion, Industrial Engineering, IE/IS-2014-05 (2014). Available also from [1]

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Information Systems Engineering, Technion, Haifa, Israel

    Michael Veksler & Ofer Strichman

Authors
  1. Michael Veksler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ofer Strichman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ofer Strichman .

Editor information

Editors and Affiliations

  1. University of Connecticut, Storrs, Connecticut, USA

    Laurent Michel

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Veksler, M., Strichman, O. (2015). Learning General Constraints in CSP. In: Michel, L. (eds) Integration of AI and OR Techniques in Constraint Programming. CPAIOR 2015. Lecture Notes in Computer Science(), vol 9075. Springer, Cham. https://doi.org/10.1007/978-3-319-18008-3_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-18008-3_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-18007-6

  • Online ISBN: 978-3-319-18008-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation