{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:19:06Z","timestamp":1740122346611,"version":"3.37.3"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T00:00:00Z","timestamp":1698883200000},"content-version":"vor","delay-in-days":62,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R513386\/1","EP\/W001977\/1"],"award-info":[{"award-number":["EP\/R513386\/1","EP\/W001977\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Constraints"],"published-print":{"date-parts":[[2023,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.<\/jats:p>","DOI":"10.1007\/s10601-023-09364-1","type":"journal-article","created":{"date-parts":[[2023,11,2]],"date-time":"2023-11-02T07:02:05Z","timestamp":1698908525000},"page":"397-426","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Learning to select SAT encodings for pseudo-Boolean and linear integer constraints"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5162-5826","authenticated-orcid":false,"given":"Felix","family":"Ulrich-Oltean","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5052-8634","authenticated-orcid":false,"given":"Peter","family":"Nightingale","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2174-7173","authenticated-orcid":false,"given":"James Alfred","family":"Walker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,2]]},"reference":[{"key":"9364_CR1","doi-asserted-by":"publisher","unstructured":"Bofill, M., Coll, J., Suy, J., & Villaret, M. (2017). Compact MDDs for Pseudo-Boolean Constraints with At-Most-One Relations in Resource-Constrained Scheduling Problems. In Proceedings of the twenty-sixth international joint conference on artificial intelligence, pp. 555\u2013562. International Joint Conferences on Artificial Intelligence Organization, Melbourne, Australia. https:\/\/doi.org\/10.24963\/ijcai.2017\/78","DOI":"10.24963\/ijcai.2017\/78"},{"key":"9364_CR2","doi-asserted-by":"publisher","unstructured":"Bofill, M., Coll, J., Suy, J., & Villaret, M. (2019). SAT encodings of pseudo-boolean constraints with at-most-one relations. In International conference on integration of constraint programming, artificial intelligence, and operations research, Springer, pp. 112\u2013128. https:\/\/doi.org\/10.1007\/978-3-030-19212-9","DOI":"10.1007\/978-3-030-19212-9"},{"key":"9364_CR3","doi-asserted-by":"publisher","first-page":"103604","DOI":"10.1016\/j.artint.2021.103604","volume":"302","author":"M Bofill","year":"2022","unstructured":"Bofill, M., Coll, J., Nightingale, P., Suy, J., Ulrich-Oltean, F., & Villaret, M. (2022). SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints. Artificial Intelligence., 302, 103604. https:\/\/doi.org\/10.1016\/j.artint.2021.103604","journal-title":"Artificial Intelligence."},{"key":"9364_CR4","doi-asserted-by":"publisher","unstructured":"Joshi, S., Martins, R., & Manquinho, V. (2015). Generalized Totalizer Encoding for Pseudo-Boolean Constraints. In G. Pesant (Ed.), Principles and practice of constraint programming. lecture notes in computer science, pp. 200\u2013209. Springer International Publishing, Cham. https:\/\/doi.org\/10.1007\/978-3-319-23219-5_15","DOI":"10.1007\/978-3-319-23219-5_15"},{"key":"9364_CR5","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1613\/jair.3653","volume":"45","author":"I Ab\u00edo","year":"2012","unstructured":"Ab\u00edo, I., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., & Mayer-Eichberger, V. (2012). A New Look at BDDs for Pseudo-Boolean Constraints. Journal of Artificial Intelligence Research, 45, 443\u2013480. https:\/\/doi.org\/10.1613\/jair.3653","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9364_CR6","doi-asserted-by":"publisher","unstructured":"Bailleux, O., Boufkhad, Y., & Roussel, O. (2009). New Encodings of Pseudo-Boolean Constraints into CNF. In O. Kullmann (Ed.), Theory and applications of satisfiability testing - SAT 2009. Lecture Notes in Computer Science, pp. 181\u2013194. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-02777-2_19","DOI":"10.1007\/978-3-642-02777-2_19"},{"key":"9364_CR7","doi-asserted-by":"publisher","unstructured":"H\u00f6lldobler, S., Manthey, N., & Steinke, P. (2012). A Compact Encoding of Pseudo-Boolean Constraints into SAT. In B. Glimm, A. Kr\u00fcger (Eds.), KI 2012: Advances in artificial intelligence. Lecture Notes in Computer Science, pp. 107\u2013118. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-33347-7_10","DOI":"10.1007\/978-3-642-33347-7_10"},{"issue":"2","key":"9364_CR8","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10601-018-9299-0","volume":"24","author":"A Zha","year":"2019","unstructured":"Zha, A., Koshimura, M., & Fujita, H. (2019). N-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT. Constraints., 24(2), 133\u2013161.","journal-title":"Constraints."},{"key":"9364_CR9","doi-asserted-by":"publisher","unstructured":"Ans\u00f3tegui, C., Bofill, M., Coll, J., Dang, N., Esteban, J. L., Miguel, I., Nightingale, P., Salamon, A. Z., Suy, J., & Villaret, M. (2019). Automatic detection of at-most-one and exactly-one relations for improved SAT encodings of pseudo-boolean constraints. In International conference on principles and practice of constraint programming, Springer, pp. 20\u201336. https:\/\/doi.org\/10.1007\/978-3-030-30048-7","DOI":"10.1007\/978-3-030-30048-7"},{"key":"9364_CR10","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.artint.2017.07.001","volume":"251","author":"P Nightingale","year":"2017","unstructured":"Nightingale, P., Akg\u00fcn, \u00d6., Gent, I. P., Jefferson, C., Miguel, I., & Spracklen, P. (2017). Automatically improving constraint models in Savile Row. Artificial Intelligence, 251, 35\u201361. https:\/\/doi.org\/10.1016\/j.artint.2017.07.001","journal-title":"Artificial Intelligence"},{"key":"9364_CR11","doi-asserted-by":"publisher","unstructured":"Davidson, E., Akg\u00fcn, \u00d6., Espasa, J., & Nightingale, P. (2020). Effective Encodings of Constraint Programming Models to SMT. In H. Simonis (Ed.), Principles and practice of constraint programming. Lecture Notes in Computer Science, pp. 143\u2013159. Springer International Publishing, Cham. https:\/\/doi.org\/10.1007\/978-3-030-58475-7_9","DOI":"10.1007\/978-3-030-58475-7_9"},{"key":"9364_CR12","doi-asserted-by":"publisher","unstructured":"Hurley, B., Kotthoff, L., Malitsky, Y., & O\u2019Sullivan, B. (2014). Proteus: A Hierarchical Portfolio of Solvers and Transformations. In H. Simonis (Ed.), Integration of AI and OR techniques in constraint programming. Lecture Notes in Computer Science, pp. 301\u2013317. Springer International Publishing, Cham. https:\/\/doi.org\/10.1007\/978-3-319-07046-9","DOI":"10.1007\/978-3-319-07046-9"},{"issue":"4","key":"9364_CR13","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/s10601-014-9165-7","volume":"19","author":"M Stojadinovi\u0107","year":"2014","unstructured":"Stojadinovi\u0107, M., & Mari\u0107, F. (2014). meSAT: Multiple encodings of CSP to SAT. Constraints, 19(4), 380\u2013403. https:\/\/doi.org\/10.1007\/s10601-014-9165-7","journal-title":"Constraints"},{"key":"9364_CR14","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1613\/jair.4726","volume":"53","author":"M Lindauer","year":"2015","unstructured":"Lindauer, M., Hoos, H. H., Hutter, F., & Schaub, T. (2015). AutoFolio: An Automatically Configured Algorithm Selector. Journal of Artificial Intelligence Research, 53, 745\u2013778. https:\/\/doi.org\/10.1613\/jair.4726","journal-title":"Journal of Artificial Intelligence Research"},{"key":"9364_CR15","doi-asserted-by":"publisher","unstructured":"Ulrich-Oltean, F., Nightingale, P., & Walker, J. A. (2022). Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints. In C. Solnon (Ed.), 28th International conference on principles and practice of constraint programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 235, pp. 38\u201313817. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany. https:\/\/doi.org\/10.4230\/LIPIcs.CP.2022.38","DOI":"10.4230\/LIPIcs.CP.2022.38"},{"key":"9364_CR16","unstructured":"De\u00a0Kleer, J. (1989). A comparison of ATMS and CSP techniques. In Proceedings of the eleventh international joint conference on artificial intelligence (IJCAI-89), pp. 290\u2013296"},{"key":"9364_CR17","unstructured":"Crawford, J. M., Baker, A. B. (1994). Experimental results on the application of satisfiability algorithms to scheduling problems. In Proceedings of the 12th national conference on artificial intelligence (AAAI-94), pp. 1092\u20131097"},{"key":"9364_CR18","unstructured":"Chen, J. (2010). A new sat encoding of the at-most-one constraint. Constraint Modelling and Reformulation: Proc."},{"issue":"2","key":"9364_CR19","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/s10601-008-9061-0","volume":"14","author":"N Tamura","year":"2009","unstructured":"Tamura, N., Taga, A., Kitagawa, S., & Banbara, M. (2009). Compiling finite linear CSP into SAT. Constraints, 14(2), 254\u2013272. https:\/\/doi.org\/10.1007\/s10601-008-9061-0","journal-title":"Constraints"},{"key":"9364_CR20","doi-asserted-by":"crossref","unstructured":"Tamura, N., Banbara, M., & Soh, T. (2013). Compiling pseudo-Boolean constraints to SAT with order encoding. In Proceedings IEEE 25th International conference on tools with artificial intelligence, pp. 1020\u20131027","DOI":"10.1109\/ICTAI.2013.153"},{"key":"9364_CR21","doi-asserted-by":"publisher","unstructured":"Ab\u00edo, I., Mayer-Eichberger, V., & Stuckey, P. J. (2015). Encoding linear constraints with implication chains to CNF. In International conference on principles and practice of constraint programming, Springer, pp. 3\u201311. https:\/\/doi.org\/10.1007\/978-3-319-23219-5_1","DOI":"10.1007\/978-3-319-23219-5_1"},{"issue":"7","key":"9364_CR22","doi-asserted-by":"publisher","first-page":"5157","DOI":"10.1007\/s10462-020-09817-6","volume":"53","author":"M Bofill","year":"2020","unstructured":"Bofill, M., Coll, J., Suy, J., & Villaret, M. (2020). An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations. Artificial Intelligence Review, 53(7), 5157\u20135188. https:\/\/doi.org\/10.1007\/s10462-020-09817-6","journal-title":"Artificial Intelligence Review"},{"key":"9364_CR23","unstructured":"Ab\u00edo, I., Mayer-Eichberger, V., & Stuckey, P. (2020). Encoding Linear Constraints into SAT. arXiv:2005.02073 [cs]."},{"key":"9364_CR24","doi-asserted-by":"publisher","unstructured":"Zhou, N. -F., & Kjellerstrand, H. (2017). Optimizing SAT encodings for arithmetic constraints. In International conference on principles and practice of constraint programming, Springer, pp. 671\u2013686. https:\/\/doi.org\/10.1007\/978-3-319-66158-2_43","DOI":"10.1007\/978-3-319-66158-2_43"},{"key":"9364_CR25","unstructured":"Nightingale, P.: Savile Row 1.9.0 Manual. https:\/\/savilerow.cs.st-andrews.ac.uk\/index.html"},{"key":"9364_CR26","doi-asserted-by":"publisher","unstructured":"Amadini, R., Gabbrielli, M., & Mauro, J. (2014). An enhanced features extractor for a portfolio of constraint solvers. In Proceedings of the 29th annual ACM symposium on applied computing. SAC \u201914, pp. 1357\u20131359. Association for Computing Machinery, New York, NY, USA. https:\/\/doi.org\/10.1145\/2554850.2555114","DOI":"10.1145\/2554850.2555114"},{"key":"9364_CR27","unstructured":"Lecoutre, C., & Roussel, O. (2019). XCSP3 Competition. http:\/\/www.cril.univ-artois.fr\/XCSP19\/"},{"key":"9364_CR28","first-page":"2825","volume":"12","author":"F Pedregosa","year":"2011","unstructured":"Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., & Duchesnay, E. (2011). Scikit-learn: Machine learning in Python. Journal of Machine Learning Research, 12, 2825\u20132830.","journal-title":"Journal of Machine Learning Research"},{"key":"9364_CR29","doi-asserted-by":"publisher","unstructured":"Chen, T., & Guestrin, C. (2016). XGBoost: A Scalable Tree Boosting System. In Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining, ACM, San Francisco California USA, pp. 785\u2013794. https:\/\/doi.org\/10.1145\/2939672.2939785","DOI":"10.1145\/2939672.2939785"},{"issue":"1","key":"9364_CR30","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman, L. (2001). Random Forests. Machine Learning, 45(1), 5\u201332. https:\/\/doi.org\/10.1023\/A:1010933404324","journal-title":"Machine Learning"},{"issue":"3","key":"9364_CR31","doi-asserted-by":"publisher","first-page":"1301","DOI":"10.1002\/widm.1301","volume":"9","author":"P Probst","year":"2019","unstructured":"Probst, P., Wright, M. N., & Boulesteix, A.-L. (2019). Hyperparameters and tuning strategies for random forest. WIREs Data Mining and Knowledge Discovery, 9(3), 1301. https:\/\/doi.org\/10.1002\/widm.1301","journal-title":"WIREs Data Mining and Knowledge Discovery"},{"issue":"1","key":"9364_CR32","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1162\/evco_a_00242","volume":"27","author":"P Kerschke","year":"2019","unstructured":"Kerschke, P., Hoos, H. H., Neumann, F., & Trautmann, H. (2019). Automated Algorithm Selection: Survey and Perspectives. Evolutionary Computation, 27(1), 3\u201345. https:\/\/doi.org\/10.1162\/evco_a_00242","journal-title":"Evolutionary Computation"},{"key":"9364_CR33","unstructured":"Heule, M., Jarvisalo, M., Suda, M., Iser, M., Balyo, T., & Froleyks, N.: SAT Competitions. https:\/\/satcompetition.github.io\/"},{"key":"9364_CR34","unstructured":"University of Helsinki, H. I. f. I. T., Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., & Suda, M. (2021). Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. In proceedings of SAT competition 2021. http:\/\/hdl.handle.net\/10138\/333647"},{"key":"9364_CR35","doi-asserted-by":"crossref","unstructured":"Soh, T., Banbara, M., & Tamura, N. (2015). A hybrid encoding of CSP to SAT integrating order and log encodings. In Proceedings IEEE 27th international conference on tools with artificial intelligence (ICTAI), pp. 421\u2013428","DOI":"10.1109\/ICTAI.2015.70"}],"container-title":["Constraints"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-023-09364-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10601-023-09364-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10601-023-09364-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,9]],"date-time":"2023-11-09T09:13:36Z","timestamp":1699521216000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10601-023-09364-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["9364"],"URL":"https:\/\/doi.org\/10.1007\/s10601-023-09364-1","relation":{},"ISSN":["1383-7133","1572-9354"],"issn-type":[{"type":"print","value":"1383-7133"},{"type":"electronic","value":"1572-9354"}],"subject":[],"published":{"date-parts":[[2023,9]]},"assertion":[{"value":"27 September 2023","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"We have reviewed ethical concerns and no further action is required.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent to participate"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}},{"value":"Not applicable.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}