{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T15:38:02Z","timestamp":1790696282823,"version":"4.1.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"8","license":[{"start":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T00:00:00Z","timestamp":1500854400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2017,7,24]]},"abstract":"<jats:p>Mathematics solves problems by pen and paper. CS helps us to go far beyond that.<\/jats:p>","DOI":"10.1145\/3107239","type":"journal-article","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T12:52:34Z","timestamp":1500900754000},"page":"70-79","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":86,"title":["The science of brute force"],"prefix":"10.1145","volume":"60","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[{"name":"The University of Texas, Austin"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[{"name":"Swansea University, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,7,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2014.05.007"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"e_1_2_1_3_1","series-title":"FAIA","volume-title":"Handbook of Satisfiability","author":"Biere A.","year":"2009","unstructured":"Biere , A. , Heule , M.J.H. , van Maaren , H. , Walsh , T. eds. Handbook of Satisfiability , volume 185 of FAIA . IOS Press , Amsterdam, The Netherlands, Feb. 2009 . Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. eds. Handbook of Satisfiability, volume 185 of FAIA. IOS Press, Amsterdam, The Netherlands, Feb. 2009."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20297-6_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_43"},{"key":"e_1_2_1_8_1","volume-title":"Efficient certified resolution proof checking","author":"Cruz-Filipe L.","year":"2016","unstructured":"Cruz-Filipe , L. , Marques-Silva , J.P. , Schneider-Kamp , P. Efficient certified resolution proof checking , 2016 . https:\/\/arxiv.org\/abs\/1610.06984. Cruz-Filipe, L., Marques-Silva, J.P., Schneider-Kamp, P. Efficient certified resolution proof checking, 2016. https:\/\/arxiv.org\/abs\/1610.06984."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"e_1_2_1_11_1","volume-title":"Computers and Intractability","author":"Garey M.R.","year":"1979","unstructured":"Garey , M.R. , Johnson , D.S. Computers and Intractability ; A Guide to the Theory of NP-Completeness. W.H. Freeman and Company , 1979 . Garey, M.R., Johnson, D.S. Computers and Intractability; A Guide to the Theory of NP-Completeness. W.H. Freeman and Company, 1979."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2003.1253718"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1038\/scientificamerican0790-112"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"e_1_2_1_16_1","volume-title":"Cube and conquer: Guiding CDCL SAT solvers by lookaheads","author":"Heule M.J.H.","year":"2011","unstructured":"Heule , M.J.H. , Kullmann , O. , Wieringa , S. , Biere , A. Cube and conquer: Guiding CDCL SAT solvers by lookaheads . In HVC (Springer , 2011 ), 50--65. Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In HVC (Springer, 2011), 50--65."},{"key":"e_1_2_1_17_1","first-page":"155","article-title":"Look-ahead based SAT solvers. In Biere et al. [3]","volume":"5","author":"Heule M.J.H.","year":"2009","unstructured":"Heule , M.J.H. , van Maaren , H . Look-ahead based SAT solvers. In Biere et al. [3] , Chapter 5 , ( 2009 ), 155 -- 184 . Heule, M.J.H., van Maaren, H. Look-ahead based SAT solvers. In Biere et al. [3], Chapter 5, (2009), 155--184.","journal-title":"Chapter"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.013"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"e_1_2_1_20_1","first-page":"185","article-title":"Incomplete algorithms. In Biere et al. [3]","volume":"6","author":"Kautz H.A.","year":"2009","unstructured":"Kautz , H.A. , Sabharwal , A. , Selman , B . Incomplete algorithms. In Biere et al. [3] , Chapter 6 , ( 2009 ), 185 -- 203 . Kautz, H.A., Sabharwal, A., Selman, B. Incomplete algorithms. In Biere et al. [3], Chapter 6, (2009), 185--203.","journal-title":"Chapter"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2015.03.004"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2008.10129025"},{"key":"e_1_2_1_23_1","first-page":"205","article-title":"Fundaments of branching heuristics. In Biere et al. [3]","volume":"7","author":"Kullmann O","year":"2009","unstructured":"Kullmann , O . Fundaments of branching heuristics. In Biere et al. [3] , Chapter 7 , ( 2009 ), 205 -- 244 . Kullmann, O. Fundaments of branching heuristics. In Biere et al. [3], Chapter 7, (2009), 205--244.","journal-title":"Chapter"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2307\/2323798"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature.2016.19990"},{"key":"e_1_2_1_26_1","series-title":"Student mathematical library","doi-asserted-by":"crossref","DOI":"10.1090\/stml\/024","volume-title":"Ramsey Theory on the Integers","author":"Landman B.M.","year":"2003","unstructured":"Landman , B.M. , Robertson , A. Ramsey Theory on the Integers , volume 24 of Student mathematical library . American Mathematical Society , Providence, RI , 2003 . Landman, B.M., Robertson, A. Ramsey Theory on the Integers, volume 24 of Student mathematical library. American Mathematical Society, Providence, RI, 2003."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39206-1_58"},{"key":"e_1_2_1_28_1","first-page":"131","article-title":"Conflict-driven clause learning SAT solvers. In Biere et al. [3]","volume":"4","author":"Marques-Silva J.P.","year":"2009","unstructured":"Marques-Silva , J.P. , Lynce , I. , Malik , S . Conflict-driven clause learning SAT solvers. In Biere et al. [3] , Chapter 4 , ( 2009 ), 131 -- 153 . Marques-Silva, J.P., Lynce, I., Malik, S. Conflict-driven clause learning SAT solvers. In Biere et al. [3], Chapter 4, (2009), 131--153.","journal-title":"Chapter"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2013.870056"},{"key":"e_1_2_1_31_1","volume-title":"versat: A verified modern SAT solver","author":"Oe D.","year":"2012","unstructured":"Oe , D. , Stump , A. , Oliver , C. , Clancy , K. versat: A verified modern SAT solver . In VMCAI (Springer 2012 ) 363--378. Oe, D., Stump, A., Oliver, C., Clancy, K. versat: A verified modern SAT solver. In VMCAI (Springer 2012) 363--378."},{"key":"e_1_2_1_32_1","volume-title":"Small Ramsey numbers. The Electronic Journal of Combinatorics (January","author":"Radziszowski S.P.","year":"2014","unstructured":"Radziszowski , S.P. Small Ramsey numbers. The Electronic Journal of Combinatorics (January 2014 ), Dynamic Surveys DS1, Revision 14. Radziszowski, S.P. Small Ramsey numbers. The Electronic Journal of Combinatorics (January 2014), Dynamic Surveys DS1, Revision 14."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_2_1_34_1","first-page":"114","article-title":"\u00dcber die Kongruenz xm + ym = zm (mod p)","volume":"25","author":"Schur I","year":"1917","unstructured":"Schur , I . \u00dcber die Kongruenz xm + ym = zm (mod p) . Jahresbericht der Deutschen Mathematiker Vereinigung 25 ( 1917 ), 114 -- 116 . Schur, I. \u00dcber die Kongruenz xm + ym = zm (mod p). Jahresbericht der Deutschen Mathematiker Vereinigung 25 (1917), 114--116.","journal-title":"Jahresbericht der Deutschen Mathematiker Vereinigung"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.19086\/da.609"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"e_1_2_1_37_1","volume-title":"Four Colors Suffice: How the Map Problem Was Solved","author":"Wilson R.","year":"2013","unstructured":"Wilson , R. Four Colors Suffice: How the Map Problem Was Solved . Princeton University Press , Princeton, NJ , revised edition, 2013 . Wilson, R. Four Colors Suffice: How the Map Problem Was Solved. Princeton University Press, Princeton, NJ, revised edition, 2013."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3107239","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3107239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:21Z","timestamp":1750217421000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3107239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,24]]},"references-count":36,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2017,7,24]]}},"alternative-id":["10.1145\/3107239"],"URL":"https:\/\/doi.org\/10.1145\/3107239","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,24]]},"assertion":[{"value":"2017-07-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}