{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T07:42:00Z","timestamp":1777016520790,"version":"3.51.4"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,8]]},"abstract":"<jats:p>A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem [Heule et al., 2016], delivering the largest proof yet, of 200 terabytes in size. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, based on integrating the \u201cold\u201d and \u201cnew\u201d methods of SAT solving.<\/jats:p>","DOI":"10.24963\/ijcai.2017\/683","type":"proceedings-article","created":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T09:14:07Z","timestamp":1501233247000},"page":"4864-4868","source":"Crossref","is-referenced-by-count":8,"title":["Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method"],"prefix":"10.24963","author":[{"given":"Marijn J.H.","family":"Heule","sequence":"first","affiliation":[{"name":"The University of Texas at Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[{"name":"Swansea University, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor W.","family":"Marek","sequence":"additional","affiliation":[{"name":"University of Kentucky"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"name":"Twenty-Sixth International Joint Conference on Artificial Intelligence","theme":"Artificial Intelligence","location":"Melbourne, Australia","acronym":"IJCAI-2017","number":"26","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)","University of Technology Sydney (UTS)","Australian Computer Society (ACS)"],"start":{"date-parts":[[2017,8,19]]},"end":{"date-parts":[[2017,8,26]]}},"container-title":["Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T11:55:06Z","timestamp":1501242906000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2017\/683"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2017,8]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2017\/683","relation":{},"subject":[],"published":{"date-parts":[[2017,8]]}}}