Advertisement

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    The HCSP Constraint Solver web page. http://tx.technion.ac.il/mveksler/HCSP/
  2. 2.
    Fourth international CSP solver competition (2009). http://cpai.ucc.ie/09/index.html
  3. 3.
    Minizinc challenge (2014). http://www.minizinc.org/challenge2014/
  4. 4.
  5. 5.
    Beckert, B., Hähnle, R., Manyá, F.: The SAT problem of signed CNF formulas, pp. 59–80 (2000)Google Scholar
  6. 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. 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. 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) CrossRefGoogle Scholar
  9. 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) CrossRefGoogle Scholar
  10. 10.
    Dechter, R.: Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artif. Intell. 41(3), 273–312 (1990)CrossRefGoogle Scholar
  11. 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. 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) CrossRefGoogle Scholar
  13. 13.
    Fujiwara, T.: iZplus - tool description (2014). http://www.minizinc.org/challenge2014/description_izplus.txt
  14. 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) CrossRefGoogle Scholar
  15. 15.
    Stuckey, P.J., Chu, G.: Structure based extended resolution for constraint programming. http://arxiv.org/abs/1306.4418
  16. 16.
    Hebrard, E.: Mistral, a constraints satisfiaction library. In: Third international CSP solver competition, pp. 31–40 (2008)Google Scholar
  17. 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. 18.
    Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reasoning 51(1), 79–108 (2013)CrossRefMathSciNetGoogle Scholar
  19. 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) CrossRefGoogle Scholar
  20. 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. 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. 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. 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) CrossRefGoogle Scholar
  24. 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) CrossRefGoogle Scholar
  25. 25.
    Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357–391 (2009)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 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) CrossRefGoogle Scholar
  27. 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. 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. 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

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Information Systems EngineeringTechnionHaifaIsrael

Personalised recommendations