{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:59:56Z","timestamp":1740099596253,"version":"3.37.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030351656"},{"type":"electronic","value":"9783030351663"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-35166-3_19","type":"book-chapter","created":{"date-parts":[[2019,11,16]],"date-time":"2019-11-16T15:01:27Z","timestamp":1573916487000},"page":"264-277","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Configuration of SAT Formulae"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8429-3570","authenticated-orcid":false,"given":"Mauro","family":"Vallati","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9034-2527","authenticated-orcid":false,"given":"Marco","family":"Maratea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,12]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_23"},{"key":"19_CR2","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the sat competition 2017. In: SAT competition 2017, Solver and Benchmark Descriptions (2017)"},{"issue":"1","key":"19_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L.: Random forests. Mach. Learn. 45(1), 5\u201332 (2001)","journal-title":"Mach. Learn."},{"key":"19_CR4","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MC.1987.1663532","volume":"20","author":"FP Brooks","year":"1987","unstructured":"Brooks, F.P.: No silver bullet: essence and accidents of software engineering. IEEE Computer 20, 10\u201319 (1987)","journal-title":"IEEE Computer"},{"key":"19_CR5","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, pp. 209\u2013224 (2008)"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1016\/j.ijar.2017.10.002","volume":"92","author":"F Cerutti","year":"2018","unstructured":"Cerutti, F., Vallati, M., Giacomin, M.: On the impact of configuration on abstract argumentation automated reasoning. Int. J. Approx. Reason. 92, 120\u2013138 (2018)","journal-title":"Int. J. Approx. Reason."},{"key":"19_CR7","unstructured":"Crawford, J., Baker, A.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Proceedings of the International Conference of the Association for the Advancement of Artificial Intelligence (AAAI), pp. 1092\u20131097 (1994)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-24318-4_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"S Falkner","year":"2015","unstructured":"Falkner, S., Lindauer, M., Hutter, F.: SpySMAC: automated configuration and performance analysis of SAT solvers. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 215\u2013222. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_16"},{"key":"19_CR9","unstructured":"Fitzgerald, T., Malitsky, Y., O\u2019Sullivan, B.: ReACTR: realtime algorithm configuration through tournament rankings. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI, pp. 304\u2013310 (2015)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-45757-7_25","volume-title":"Logics in Artificial Intelligence","author":"E Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A.: Dependent and independent variables in propositional satisfiability. In: Flesca, S., Greco, S., Ianni, G., Leone, N. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 296\u2013307. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45757-7_25"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"842","DOI":"10.1007\/978-3-540-45193-8_64","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"E Giunchiglia","year":"2003","unstructured":"Giunchiglia, E., Maratea, M., Tacchella, A.: (In)Effectiveness of look-ahead techniques in a modern SAT solver. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 842\u2013846. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45193-8_64"},{"issue":"1","key":"19_CR12","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"CP Gomes","year":"2000","unstructured":"Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. J. Autom. Reason. 24(1), 67\u2013100 (2000)","journal-title":"J. Autom. Reason."},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/978-3-642-25566-3_40","volume-title":"Learning and Intelligent Optimization","author":"F Hutter","year":"2011","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507\u2013523. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25566-3_40"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10472-010-9191-0","volume":"60","author":"F Hutter","year":"2010","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: Tradeoffs in the empirical evaluation of competing algorithm designs. Ann. Math. Artif. Intell. 60(1), 65\u201389 (2010)","journal-title":"Ann. Math. Artif. Intell."},{"key":"19_CR15","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K.: An efficient approach for assessing hyperparameter importance. In: Proceedings of the 31st International Conference on Machine Learning, pp. 754\u2013762 (2014)"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1613\/jair.2861","volume":"36","author":"F Hutter","year":"2009","unstructured":"Hutter, F., Hoos, H.H., Leyton-Brown, K., St\u00fctzle, T.: ParamILS: an automatic algorithm configuration framework. J. Artif. Intell. Res. 36, 267\u2013306 (2009)","journal-title":"J. Artif. Intell. Res."},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2016.09.006","volume":"243","author":"F Hutter","year":"2017","unstructured":"Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H.H., Leyton-Brown, K.: The configurable SAT solver challenge (CSSC). Artif. Intell. 243, 1\u201325 (2017)","journal-title":"Artif. Intell."},{"key":"19_CR18","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.artint.2013.10.003","volume":"206","author":"F Hutter","year":"2014","unstructured":"Hutter, F., Xu, L., Hoos, H.H., Leyton-Brown, K.: Algorithm runtime prediction: methods & evaluation. Artif. Intell. 206, 79\u2013111 (2014)","journal-title":"Artif. Intell."},{"key":"19_CR19","unstructured":"Kadioglu, S., Malitsky, Y., Sellmann, M., Tierney, K.: ISAC-instance-specific algorithm configuration. In: Proceedings of the 9th European Conference on Artificial Intelligence ECAI, pp. 751\u2013756 (2010)"},{"key":"19_CR20","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.artint.2015.11.002","volume":"232","author":"AR KhudaBukhsh","year":"2016","unstructured":"KhudaBukhsh, A.R., Xu, L., Hoos, H.H., Leyton-Brown, K.: SATenstein: automatically building local search SAT solvers from components. Artif. Intell. 232, 20\u201342 (2016)","journal-title":"Artif. Intell."},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-63516-3_15","volume-title":"Handbook of Parallel Constraint Reasoning","author":"M Lindauer","year":"2018","unstructured":"Lindauer, M., Hoos, H., Hutter, F., Leyton-Brown, K.: Selection and configuration of parallel portfolios. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 583\u2013615. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_15"},{"issue":"2","key":"19_CR22","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"MR Prasad","year":"2005","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2), 156\u2013173 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR23","unstructured":"Rintanen, J.: Engineering efficient planners with SAT. In: European Conference on Artificial Intelligence ECAI, pp. 684\u2013689 (2012)"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-642-21581-0_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"DAD Tompkins","year":"2011","unstructured":"Tompkins, D.A.D., Balint, A., Hoos, H.H.: Captain Jack: new variable selection heuristics in local search for SAT. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 302\u2013316. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_24"},{"key":"19_CR25","unstructured":"Vallati, M., Hutter, F., Chrpa, L., McCluskey, T.: On the effective configuration of planning domain models. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pp. 1704\u20131711 (2015)"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Vallati, M., Serina, I.: A general approach for configuring PDDL problem models. In: Proceedings of the International Conference on Automated Planning & Scheduling (ICAPS) (2018)","DOI":"10.1609\/icaps.v28i1.13869"},{"key":"19_CR27","unstructured":"Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, 9\u201315 August 2003, pp. 1173\u20131178. Morgan Kaufmann (2003)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Xu, L., Hoos, H.H., Leyton-Brown, K.: Hydra: automatically configuring algorithms for portfolio-based selection. In: Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI (2010)","DOI":"10.1609\/aaai.v24i1.7565"}],"container-title":["Lecture Notes in Computer Science","AI*IA 2019 \u2013 Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-35166-3_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,5]],"date-time":"2022-10-05T20:16:27Z","timestamp":1665000987000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-35166-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030351656","9783030351663"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-35166-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"AI*IA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference of the Italian Association for Artificial Intelligence","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rende","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"19 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aiia2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/aiia2019.mat.unical.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}