{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T18:44:29Z","timestamp":1744310669557,"version":"3.28.0"},"reference-count":41,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1109\/ssci.2017.8280953","type":"proceedings-article","created":{"date-parts":[[2018,2,7]],"date-time":"2018-02-07T21:44:37Z","timestamp":1518039877000},"page":"1-8","source":"Crossref","is-referenced-by-count":6,"title":["Improving performance of CDCL SAT solvers by automated design of variable selection heuristics"],"prefix":"10.1109","author":[{"given":"Marketa","family":"Illetskova","sequence":"first","affiliation":[]},{"given":"Alex R.","family":"Bertels","sequence":"additional","affiliation":[]},{"given":"Joshua M.","family":"Tuggle","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Harter","sequence":"additional","affiliation":[]},{"given":"Samuel","family":"Richter","sequence":"additional","affiliation":[]},{"given":"Daniel R.","family":"Tauritz","sequence":"additional","affiliation":[]},{"given":"Samuel","family":"Mulder","sequence":"additional","affiliation":[]},{"given":"Denis","family":"Bueno","sequence":"additional","affiliation":[]},{"given":"Michelle","family":"Leger","sequence":"additional","affiliation":[]},{"given":"William M.","family":"Siever","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","first-page":"72","article-title":"SAT Challenge 2012 Random SAT Track: Description of Benchmark Generation","author":"balint","year":"2012","journal-title":"Proceedings of SAT Challenge 2012 Solver and Benchmark Descriptions"},{"journal-title":"Configurable SAT Solver Challenge (CSSC) 2014 — Benchmarks","year":"0","key":"ref38"},{"journal-title":"A Field Guide to Genetic Programming","year":"2008","author":"poli","key":"ref33"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2739482.2768457"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2598394.2609872"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1057\/jors.2013.71"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44874-8"},{"journal-title":"Clause Learning in SAT","year":"0","author":"tichy","key":"ref36"},{"key":"ref35","article-title":"Glucose and Syrup in the SAT Race 2015","author":"audemard","year":"2015","journal-title":"Reports on the SAT 2015 Competition"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2015.7139953"},{"journal-title":"Lingeling and Friends Entering the SAT Race 2015","year":"2015","author":"biere","key":"ref40"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/11499107_25"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"229","DOI":"10.3233\/SAT190025","article-title":"Back to the SAT05 Competition: an a Posteriori Analysis of Solver Performance on Industrial Benchmarks","volume":"2","author":"zarpas","year":"2006","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2006.07.016"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1613\/jair.2861","article-title":"ParamILS: An Automatic Algorithm Configuration Framework","volume":"36","author":"hutter","year":"2009","journal-title":"Journal of Artificial Intelligence Research"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25566-3_40"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_16"},{"key":"ref17","first-page":"517","article-title":"SATenstein: Automatically Building Local Search SAT Solvers from Components","author":"khudabukhsh","year":"2009","journal-title":"Proceedings of the 21st International Jont Conference on Artifical Intelligence"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79305-2_4"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/11729976_30"},{"key":"ref28","first-page":"53","article-title":"SATzilla2009: An Automatic Algorithm Portfolio for SAT","author":"xu","year":"2009","journal-title":"SAT 2009 Competitive Events Booklet"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2012.04.020"},{"key":"ref27","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1613\/jair.2490","article-title":"SATzilla: Portfolio-Based Algorithm Selection for SAT","volume":"32","author":"xu","year":"2008","journal-title":"Journal of Artificial Intelligence Research"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1186\/1471-2105-9-S6-S6"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2010.5457017"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2013.10.003"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1023\/B:AUSE.0000038938.10589.b9"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2737095.2737115"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TSG.2012.2214407"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907707"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2008.4605925"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24855-2_59"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/CEC.2009.4983117"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1162\/evco.2008.16.1.31"},{"key":"ref24","article-title":"Evaluating CDCL Restart Schemes","author":"biere","year":"2015","journal-title":"Proceedings of the International Workshop on Pragmatics of SAT (POS'15)"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/2739480.2754752"},{"key":"ref23","first-page":"425","article-title":"Evaluating CDCL Variable Scoring Schemes","volume":"9340","year":"2015","journal-title":"SAT"},{"journal-title":"Automated Design of Boolean Satisfiability Solvers Employing Evolutionary Computation","year":"2016","author":"bertels","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2908961.2931729"}],"event":{"name":"2017 IEEE Symposium Series on Computational Intelligence (SSCI)","start":{"date-parts":[[2017,11,27]]},"location":"Honolulu, HI","end":{"date-parts":[[2017,12,1]]}},"container-title":["2017 IEEE Symposium Series on Computational Intelligence (SSCI)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8267146\/8280782\/08280953.pdf?arnumber=8280953","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,27]],"date-time":"2020-10-27T21:51:15Z","timestamp":1603835475000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8280953\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11]]},"references-count":41,"URL":"https:\/\/doi.org\/10.1109\/ssci.2017.8280953","relation":{},"subject":[],"published":{"date-parts":[[2017,11]]}}}