{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T04:14:25Z","timestamp":1747973665945,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319180076"},{"type":"electronic","value":"9783319180083"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-18008-3_28","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T07:32:51Z","timestamp":1429083171000},"page":"410-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Learning General Constraints in CSP"],"prefix":"10.1007","author":[{"given":"Michael","family":"Veksler","sequence":"first","affiliation":[]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"28_CR1","unstructured":"The HCSP Constraint Solver web page. http:\/\/tx.technion.ac.il\/mveksler\/HCSP\/"},{"key":"28_CR2","unstructured":"Fourth international CSP solver competition (2009). http:\/\/cpai.ucc.ie\/09\/index.html"},{"key":"28_CR3","unstructured":"Minizinc challenge (2014). http:\/\/www.minizinc.org\/challenge2014\/"},{"key":"28_CR4","unstructured":"Opturion CPX - tool description (2014). http:\/\/www.minizinc.org\/challenge2014\/description_opturion_cpx.txt"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Many\u00e1, F.: The SAT problem of signed CNF formulas, pp. 59\u201380 (2000)","DOI":"10.1007\/978-94-011-4040-9_3"},{"key":"28_CR6","unstructured":"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\u2013481. IOS Press (2009)"},{"key":"28_CR7","unstructured":"Boussemart, F., Hemery, F., Lecoutre, C., Sais, L.: Boosting systematic search by weighting constraints. In: L\u00f3pez de M\u00e1ntaras, R., Saitta, L. (eds.) ECAI, pp. 146\u2013150. IOS Press (2004)"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11941439_9","volume-title":"AI 2006: Advances in Artificial Intelligence","author":"CW Choi","year":"2006","unstructured":"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\u201358. Springer, Heidelberg (2006)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11814948_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S Cotton","year":"2006","unstructured":"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\u2013183. Springer, Heidelberg (2006)"},{"issue":"3","key":"28_CR10","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(90)90046-3","volume":"41","author":"R Dechter","year":"1990","unstructured":"Dechter, R.: Enhancement schemes for constraint processing: backjumping, learning, and cutset decomposition. Artif. Intell. 41(3), 273\u2013312 (1990)","journal-title":"Artif. Intell."},{"key":"28_CR11","unstructured":"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\u2013640. AAAI Press \/ The MIT Press (2002)"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-04244-7_29","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"T Feydy","year":"2009","unstructured":"Feydy, T., Stuckey, P.J.: Lazy clause generation reengineered. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 352\u2013366. Springer, Heidelberg (2009)"},{"key":"28_CR13","unstructured":"Fujiwara, T.: iZplus - tool description (2014). http:\/\/www.minizinc.org\/challenge2014\/description_izplus.txt"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-11503-5_19","volume-title":"Practical Aspects of Declarative Languages","author":"IP Gent","year":"2010","unstructured":"Gent, I.P., Miguel, I., Moore, N.C.A.: Lazy explanations for constraint propagators. In: Carro, M., Pe\u00f1a, R. (eds.) PADL 2010. LNCS, vol. 5937, pp. 217\u2013233. Springer, Heidelberg (2010)"},{"key":"28_CR15","unstructured":"Stuckey, P.J., Chu, G.: Structure based extended resolution for constraint programming. http:\/\/arxiv.org\/abs\/1306.4418"},{"key":"28_CR16","unstructured":"Hebrard, E.: Mistral, a constraints satisfiaction library. In: Third international CSP solver competition, pp. 31\u201340 (2008)"},{"key":"28_CR17","unstructured":"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\u201311, 2011. AAAI Press (2011)"},{"issue":"1","key":"28_CR18","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovic","year":"2013","unstructured":"Jovanovic, D., de Moura, L.M.: Cutting to the chase - solving linear integer arithmetic. J. Autom. Reasoning 51(1), 79\u2013108 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"873","DOI":"10.1007\/978-3-540-45193-8_70","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"G Katsirelos","year":"2003","unstructured":"Katsirelos, G., Bacchus, F.: Unrestricted nogood recording in CSP search. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 873\u2013877. Springer, Heidelberg (2003)"},{"key":"28_CR20","unstructured":"Katsirelos, G., Bacchus, F.: Generalized nogoods in CSPs. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 390\u2013396. AAAI Press \/ The MIT Press (2005)"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Liu, C., Kuehlmann, A., Moskewicz, M.W.: CAMA: a multi-valued satisfiability solver. In: ICCAD, pp. 326\u2013333. IEEE Computer Society \/ ACM (2003)","DOI":"10.1109\/ICCAD.2003.159707"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. Design Automation Conference (DAC 2001) (2001)","DOI":"10.1145\/378239.379017"},{"key":"28_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.R.: MiniZinc: towards a Standard CP Modelling Language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007)"},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/978-3-319-10428-7_42","volume-title":"Principles and Practice of Constraint Programming","author":"R Nieuwenhuis","year":"2014","unstructured":"Nieuwenhuis, R.: The IntSat method for integer linear programming. In: O\u2019Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 574\u2013589. Springer, Heidelberg (2014)"},{"issue":"3","key":"28_CR25","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10601-008-9064-x","volume":"14","author":"O Ohrimenko","year":"2009","unstructured":"Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357\u2013391 (2009)","journal-title":"Constraints"},{"key":"28_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/10722167_36","volume-title":"Computer Aided Verification","author":"O Strichman","year":"2000","unstructured":"Strichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480\u2013494. Springer, Heidelberg (2000)"},{"key":"28_CR27","doi-asserted-by":"crossref","unstructured":"Veksler, M., Strichman, O.: A proof-producing CSP solver. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (2010)","DOI":"10.1609\/aaai.v24i1.7543"},{"key":"28_CR28","unstructured":"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]"},{"key":"28_CR29","unstructured":"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]"}],"container-title":["Lecture Notes in Computer Science","Integration of AI and OR Techniques in Constraint Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-18008-3_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T15:17:31Z","timestamp":1747927051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-18008-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319180076","9783319180083"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-18008-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}