{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:57:15Z","timestamp":1790927835277,"version":"4.1.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030412579","type":"print"},{"value":"9783030412586","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","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":[[2020]]},"DOI":"10.1007\/978-3-030-41258-6_15","type":"book-chapter","created":{"date-parts":[[2020,2,27]],"date-time":"2020-02-27T04:02:38Z","timestamp":1582776158000},"page":"205-219","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Effective Problem Solving Using SAT Solvers"],"prefix":"10.1007","author":[{"given":"Curtis","family":"Bright","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00fcrgen","family":"Gerhard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilias","family":"Kotsireas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,2,28]]},"reference":[{"issue":"9","key":"15_CR1","doi-asserted-by":"publisher","first-page":"793","DOI":"10.1080\/00029890.1999.12005124","volume":"106","author":"AF Archer","year":"1999","unstructured":"Archer, A.F.: A modern treatment of the 15 puzzle. Am. Math. Mon. 106(9), 793\u2013799 (1999)","journal-title":"Am. Math. Mon."},{"issue":"1","key":"15_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.disc.2007.12.043","volume":"309","author":"J Bell","year":"2009","unstructured":"Bell, J., Stevens, B.: A survey of known results and research areas for $$n$$-queens. Discret. Math. 309(1), 1\u201331 (2009)","journal-title":"Discret. Math."},{"key":"15_CR3","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T.: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.4153\/CJM-1960-016-5","volume":"12","author":"RC Bose","year":"1960","unstructured":"Bose, R.C., Shrikhande, S.S., Parker, E.T.: Further results on the construction of mutually orthogonal Latin squares and the falsity of Euler\u2019s conjecture. Can. J. Math. 12, 189\u2013203 (1960)","journal-title":"Can. J. Math."},{"issue":"5","key":"15_CR5","doi-asserted-by":"publisher","first-page":"734","DOI":"10.1073\/pnas.45.5.734","volume":"45","author":"RC Bose","year":"1959","unstructured":"Bose, R.C., Shrikhande, S.S.: On the falsity of Euler\u2019s conjecture about the non-existence of two orthogonal Latin squares of order $$4t+2$$. Proc. Natl. Acad. Sci. U.S.A. 45(5), 734\u2013737 (1959)","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"key":"15_CR6","unstructured":"Bright, C.: Maple applications by Curtis Bright. https:\/\/www.maplesoft.com\/applications\/Author.aspx?mid=345070"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Bright, C., Kotsireas, I., Ganesh, V.: A SAT+CAS method for enumerating Williamson matrices of even order. In: McIlraith, S., Weinberger, K. (eds.) Thirty-Second AAAI Conference on Artificial Intelligence, pp. 6573\u20136580. AAAI Press (2018)","DOI":"10.1609\/aaai.v32i1.12203"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1023\/A:1018972901171","volume":"90","author":"A Br\u00fcngger","year":"1999","unstructured":"Br\u00fcngger, A., Marzetta, A., Fukuda, K., Nievergelt, J.: The parallel search bench ZRAM and its applications. Ann. Oper. Res. 90, 45\u201363 (1999)","journal-title":"Ann. Oper. Res."},{"key":"15_CR9","unstructured":"Collins, N.: World\u2019s hardest sudoku: can you crack it? (2012). https:\/\/www.telegraph.co.uk\/news\/science\/science-news\/9359579\/Worlds-hardest-sudoku-can-you-crack-it.html"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"key":"15_CR11","unstructured":"Euler, L.: Recherches sur un nouvelle esp\u00e9ce de quarr\u00e9s magiques. Verhandelingen uitgegeven door het zeeuwsch Genootschap der Wetenschappen te Vlissingen, pp. 85\u2013239 (1782)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving very hard problems: cube-and-conquer, a hybrid SAT solving method. In: Sierra, C. (ed.) Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pp. 4864\u20134868. IJCAI (2017)","DOI":"10.24963\/ijcai.2017\/683"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Johnson, D.S., Trick, M.A.: Cliques, coloring, and satisfiability: second DIMACS implementation challenge, 11\u201313 October 1993, vol. 26. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/026"},{"key":"15_CR14","volume-title":"Combinatorial Algorithms: Generation, Enumeration, and Search. Discrete Mathematics and Its Applications","author":"D Kreher","year":"1998","unstructured":"Kreher, D., Stinson, D.: Combinatorial Algorithms: Generation, Enumeration, and Search. Discrete Mathematics and Its Applications. Taylor & Francis, Routledge (1998)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-66263-3_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"JH Liang","year":"2017","unstructured":"Liang, J.H., Govind V.K., H., Poupart, P., Czarnecki, K., Ganesh, V.: An empirical study of branching heuristics through the lens of global learning rate. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 119\u2013135. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_8 . https:\/\/ece.uwaterloo.ca\/maplesat\/"},{"key":"15_CR16","unstructured":"Lynce, I., Ouaknine, J.: Sudoku as a SAT problem. In: 9th International Symposium on Artificial Intelligence and Mathematics (2006)"},{"issue":"2","key":"15_CR17","doi-asserted-by":"publisher","first-page":"221","DOI":"10.2307\/1967920","volume":"23","author":"HF MacNeish","year":"1922","unstructured":"MacNeish, H.F.: Euler squares. Ann. Math. 23(2), 221\u2013227 (1922)","journal-title":"Ann. Math."},{"issue":"3","key":"15_CR18","first-page":"16","volume":"5","author":"BA Nadel","year":"1990","unstructured":"Nadel, B.A.: Representation selection for constraint satisfaction: a case study using $$n$$-queens. IEEE Intell. Syst. 5(3), 16\u201323 (1990)","journal-title":"IEEE Intell. Syst."},{"key":"15_CR19","unstructured":"Peterson, J.: Les 36 officieurs. Annuaire des Math\u00e9maticiens, pp. 413\u2013427 (1902)"},{"key":"15_CR20","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2010","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Pearson Education, London (2010)"},{"key":"15_CR21","volume-title":"The 15 Puzzle: How It Drove the World Crazy","author":"J Slocum","year":"2006","unstructured":"Slocum, J., Sonneveld, D.: The 15 Puzzle: How It Drove the World Crazy. Slocum Puzzle Foundation, Beverly Hills (2006)"},{"key":"15_CR22","unstructured":"Tarry, G.: Le probl\u00e8me des 36 officiers. Association Fran\u00e7aise pour l\u2019Avancement des Sciences: Compte Rendu de la 29$${\\text{me}}$$ session en Paris 1900, pp. 170\u2013203 (1901)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-1-4899-5327-8_25","volume-title":"Studies in Constructive Mathematics and Mathematical Logic Part 2","author":"G. S. Tseitin","year":"1970","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1970)"},{"key":"15_CR24","first-page":"264","volume":"19","author":"P Wernicke","year":"1910","unstructured":"Wernicke, P.: Das Problem der 36 Offiziere. Jahresbericht der Deutschen Mathematiker-Vereinigung 19, 264\u2013267 (1910)","journal-title":"Jahresbericht der Deutschen Mathematiker-Vereinigung"},{"issue":"11","key":"15_CR25","first-page":"4","volume":"3","author":"O Zaikin","year":"2015","unstructured":"Zaikin, O., Kochemazov, S.: The search for systems of diagonal Latin squares using the SAT@home project. Int. J. Open Inf. Technol. 3(11), 4\u20139 (2015)","journal-title":"Int. J. Open Inf. Technol."}],"container-title":["Communications in Computer and Information Science","Maple in Mathematics Education and Research"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-41258-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,16]],"date-time":"2022-10-16T14:43:52Z","timestamp":1665931432000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-41258-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030412579","9783030412586"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-41258-6_15","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"value":"1865-0929","type":"print"},{"value":"1865-0937","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"28 February 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Maple Conference","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Waterloo, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.maplesoft.com\/mapleconference\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"59% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"-","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1 contributed paper by the Plenary\/Invited Speaker","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}