{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:42:22Z","timestamp":1762101742893,"version":"3.41.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_41","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"607-622","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers"],"prefix":"10.1007","author":[{"given":"Edward","family":"Zulkoski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krzysztof","family":"Czarnecki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"41_CR1","first-page":"399","volume":"9","author":"G Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. IJCAI 9, 399\u2013404 (2009)","journal-title":"IJCAI"},{"key":"41_CR2","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)"},{"key":"41_CR3","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T.(eds.): Handbook of Satisfiability. FAIA, vol. 185. IOS Press (February 2009)"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"Bouton, T., de Oliveira, D.C.B., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: CADE (2009)","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"41_CR5","unstructured":"Chen, Y-C., Li, K-L.: Matchings extend to perfect matchings on hypercube networks. In: IMECS, vol. 1. Citeseer (2010)"},{"key":"41_CR6","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 de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"41_CR7","unstructured":"Devos, M., Norine, S.: Edge-antipodal Colorings of Cubes. http:\/\/garden.irmacs.sfu.ca\/?q=op\/edge_antipodal_colorings_of_cubes"},{"key":"41_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11564751_18","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"G Dooms","year":"2005","unstructured":"Dooms, G., Deville, Y., Dupont, P.E.: CP(Graph): introducing a graph computation domain in constraint programming. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 211\u2013225. Springer, Heidelberg (2005)"},{"issue":"10","key":"41_CR9","doi-asserted-by":"publisher","first-page":"1421","DOI":"10.1016\/j.dam.2012.12.025","volume":"161","author":"T Feder","year":"2013","unstructured":"Feder, T., Subi, C.: On hypercube labellings and antipodal monochromatic paths. Discrete Appl. Math. 161(10), 1421\u20131426 (2013)","journal-title":"Discrete Appl. Math."},{"issue":"6","key":"41_CR10","doi-asserted-by":"publisher","first-page":"1074","DOI":"10.1016\/j.jctb.2007.02.007","volume":"97","author":"J Fink","year":"2007","unstructured":"Fink, J.: Perfect matchings extend to hamilton cycles in hypercubes. J. Comb. Theor. B 97(6), 1074\u20131076 (2007)","journal-title":"J. Comb. Theor. B"},{"issue":"2","key":"41_CR11","doi-asserted-by":"publisher","first-page":"1100","DOI":"10.1137\/070697288","volume":"23","author":"J Fink","year":"2009","unstructured":"Fink, J.: Connectivity of matching graph of hypercube. SIDMA 23(2), 1100\u20131109 (2009)","journal-title":"SIDMA"},{"key":"41_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"41_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-31612-8_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"V Ganesh","year":"2012","unstructured":"Ganesh, V., O\u2019Donnell, C.W., Soos, M., Devadas, S., Rinard, M.C., Solar-Lezama, A.: Lynx: a programmatic sat solver for the rna-folding problem. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 143\u2013156. Springer, Heidelberg (2012)"},{"key":"41_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-319-11558-0_10","volume-title":"Logics in Artificial Intelligence","author":"M Gebser","year":"2014","unstructured":"Gebser, M., Janhunen, T., Rintanen, J.: SAT modulo graphs: acyclicity. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS, vol. 8761, pp. 137\u2013151. Springer, Heidelberg (2014)"},{"issue":"6","key":"41_CR15","doi-asserted-by":"publisher","first-page":"1711","DOI":"10.1016\/j.disc.2008.02.013","volume":"309","author":"P Gregor","year":"2009","unstructured":"Gregor, P.: Perfect matchings extending on subcubes to hamiltonian cycles of hypercubes. Discrete Math. 309(6), 1711\u20131713 (2009)","journal-title":"Discrete Math."},{"key":"41_CR16","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: FMCAD, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"issue":"4","key":"41_CR17","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1145\/502090.502095","volume":"48","author":"J Holm","year":"2001","unstructured":"Holm, J., De Lichtenberg, K., Thorup, M.: Poly-logarithmic deterministic fully-dynamic algorithms for connectivity, minimum spanning tree, 2-edge, and biconnectivity. J. ACM (JACM) 48(4), 723\u2013760 (2001)","journal-title":"J. ACM (JACM)"},{"key":"41_CR18","doi-asserted-by":"crossref","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the Erd\u0151s discrepancy conjecture. In: SAT (2014)","DOI":"10.1007\/978-3-319-09284-3_17"},{"key":"41_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-32275-7_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 36\u201350. Springer, Heidelberg (2005)"},{"issue":"1","key":"41_CR20","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1137\/0406012","volume":"6","author":"F Ruskey","year":"1993","unstructured":"Ruskey, F., Savage, C.: Hamilton cycles that extend transposition matchings in Cayley graphs of $$S_n$$. SIDMA 6(1), 152\u2013166 (1993)","journal-title":"SIDMA"},{"key":"41_CR21","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisfiability Boolean Model. Comput. 3, 141\u2013224 (2007)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"41_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1007\/978-3-319-11558-0_52","volume-title":"Logics in Artificial Intelligence","author":"T Soh","year":"2014","unstructured":"Soh, T., Le Berre, D., Roussel, S., Banbara, M., Tamura, N.: Incremental SAT-based method with native boolean cardinality handling for the hamiltonian cycle problem. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS, vol. 8761, pp. 684\u2013693. Springer, Heidelberg (2014)"},{"key":"41_CR23","unstructured":"Stein, W.A.(et al).: Sage Mathematics Software (Version 6.3) (2010)"},{"key":"41_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11814948_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Thurley","year":"2006","unstructured":"Thurley, M.: sharpSAT \u2013 counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424\u2013429. Springer, Heidelberg (2006)"},{"key":"41_CR25","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Gao, P.: Efficient SAT techniques for absolute encoding of permutation problems: application to hamiltonian cycles. In: SARA (2009)","DOI":"10.1007\/978-3-642-10439-8_52"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T17:11:11Z","timestamp":1748538671000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_41","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":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}