{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:46:13Z","timestamp":1768164373584,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319733043","type":"print"},{"value":"9783319733050","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,22]],"date-time":"2017-12-22T00:00:00Z","timestamp":1513900800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-73305-0_5","type":"book-chapter","created":{"date-parts":[[2017,12,21]],"date-time":"2017-12-21T11:05:50Z","timestamp":1513854350000},"page":"63-79","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Three Is a Crowd: SAT, SMT and CLP on a Chessboard"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-9798","authenticated-orcid":false,"given":"Sebastian","family":"Krings","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9952-0214","authenticated-orcid":false,"given":"Stefan","family":"Hallerstede","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7320-7684","authenticated-orcid":false,"given":"Miran","family":"Hasanagi\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,22]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 167\u2013180. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02777-2_18"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45193-8_8"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0033845","volume-title":"Programming Languages: Implementations, Logics, and Programs","author":"M Carlsson","year":"1997","unstructured":"Carlsson, M., Ottosson, G., Carlson, B.: An open-ended finite domain constraint solver. In: Glaser, H., Hartel, P., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191\u2013206. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/BFb0033845"},{"issue":"2","key":"5_CR6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1287\/ited.2.2.56","volume":"2","author":"MJ Chlond","year":"2002","unstructured":"Chlond, M.J.: IP modeling of chessboard placements and related puzzles. INFORMS Trans. Educ. 2(2), 56\u201357 (2002)","journal-title":"INFORMS Trans. Educ."},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-30885-7_14","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D D\u00e9harbe","year":"2012","unstructured":"D\u00e9harbe, D., Fontaine, P., Guyot, Y., Voisin, L.: SMT solvers for Rodin. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 194\u2013207. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-30885-7_14"},{"key":"5_CR9","unstructured":"Dudeney, H.E.: Amusements in Mathematics (1917). \nhttps:\/\/www.gutenberg.org\/ebooks\/16713"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"issue":"6","key":"5_CR11","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1049\/sej.1989.0045","volume":"4","author":"I Hayes","year":"1989","unstructured":"Hayes, I., Jones, C.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330\u2013338 (1989)","journal-title":"Softw. Eng. J."},{"key":"5_CR12","doi-asserted-by":"crossref","DOI":"10.1002\/9781118033036","volume-title":"Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction","author":"JN Hooker","year":"2000","unstructured":"Hooker, J.N.: Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction. John Wiley, New York (2000)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-33600-8_8","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"S Krings","year":"2016","unstructured":"Krings, S., Leuschel, M.: Proof assisted symbolic model checking for B and event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 135\u2013150. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33600-8_8"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-49815-7_1","volume-title":"Formal Methods: Foundations and Applications","author":"M Leuschel","year":"2016","unstructured":"Leuschel, M.: Formal model-based constraint solving and document generation. In: Ribeiro, L., Lecomte, T. (eds.) SBMF 2016. LNCS, vol. 10090, pp. 3\u201320. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-49815-7_1"},{"issue":"2","key":"5_CR15","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185\u2013203 (2008)","journal-title":"STTT"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-662-43652-3_8","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014","author":"M Leuschel","year":"2014","unstructured":"Leuschel, M., Schneider, D.: Towards B as a high-level constraint modelling language. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 101\u2013116. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_8"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Luo, M., Li, C.-M., Xiao, F., Many\u00e0, F., L\u00fc, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings IJCAI-2017, pp. 703\u2013711 (2017)","DOI":"10.24963\/ijcai.2017\/98"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-28717-6_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Merz","year":"2012","unstructured":"Merz, S., Vanzetto, H.: Automatic verification of TLA+ proof obligations with SMT solvers. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 289\u2013303. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28717-6_23"},{"key":"5_CR19","unstructured":"OscaR Team. OscaR: Scala in OR (2012). \nhttps:\/\/bitbucket.org\/oscarlib\/oscar"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-32759-9_31","volume-title":"FM 2012: Formal Methods","author":"D Plagge","year":"2012","unstructured":"Plagge, D., Leuschel, M.: Validating B, Z and TLA\n          + using ProB\u00a0and Kodkod. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 372\u2013386. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32759-9_31"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-22969-0_10","volume-title":"Software Engineering and Formal Methods","author":"A Savary","year":"2015","unstructured":"Savary, A., Frappier, M., Leuschel, M., Lanet, J.-L.: Model-based robustness testing in Event-B using mutation. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 132\u2013147. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-22969-0_10"},{"issue":"1\u20132","key":"5_CR22","first-page":"127","volume":"12","author":"J Schimpf","year":"2012","unstructured":"Schimpf, J., Shen, K.: ECLiPSe - from LP to CLP. TPLP 12(1\u20132), 127\u2013156 (2012)","journal-title":"TPLP"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-19249-9_30","volume-title":"FM 2015: Formal Methods","author":"D Schneider","year":"2015","unstructured":"Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487\u2013495. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_30"},{"key":"5_CR24","unstructured":"Shapiro, S.C.: The jobs puzzle: a challenge for logical expressibility and automated reasoning. In: AAAI SS (2011)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1007\/11564751_46","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"K Shen","year":"2005","unstructured":"Shen, K., Schimpf, J.: Eplex: harnessing mathematical programming solvers for constraint logic programming. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 622\u2013636. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11564751_46"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632\u2013647. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_49"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73305-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,21]],"date-time":"2017-12-21T11:07:52Z","timestamp":1513854472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73305-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,22]]},"ISBN":["9783319733043","9783319733050"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73305-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,22]]}}}