{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:08:20Z","timestamp":1784200100174,"version":"3.55.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>The Satisfiability Modulo Theory (SMT) problem over floating-point operations presents a significant challenge. State-of-the-art SMT solvers often run into difficulties when dealing with large, complex floating-point constraints. Recently, a new approach to floating-point constraint solving emerges, utilizing mathematical optimization (MO) methods as an engine of their solving approach.<\/jats:p>\n                  <jats:p>\n                    Despite the novelty, these methods can fall short in both effectiveness and efficiency due to issues of the translated functions (\n                    <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n                    ., discontinuity) and inherent limitations of their underlying MO method (\n                    <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n                    ., imprecise search process, scalability issues).\n                  <\/jats:p>\n                  <jats:p>\n                    Driven by these weaknesses of prior solvers, this paper introduces a new MO-based approach that is shown highly potent in solving floating-point constraints. Specifically, on the benchmarks of JFS (a recent solver based on fuzzing), Grater, a realization of our approach, solves as many constraints as Bitwuzla and one more than CVC5 but runs over 10 times faster and over 40 times faster than Bitwuzla and CVC5 in median solving time across all benchmarks. It is worth mentioning that Bitwuzla and CVC5 are the strongest solvers for floating-point constraints according to results of the annual international SMT solver competition (SMT-COMP). Together, they have won all gold medals for\n                    <jats:italic toggle=\"yes\">QF_FPArith<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">FPArith<\/jats:italic>\n                    divisions, which focus on floating-point constraints solving, over the past three years. To further evaluate Grater, we select over 100 most difficult benchmarks from the\n                    <jats:italic toggle=\"yes\">FP<\/jats:italic>\n                    SMT-LIB, a logic regularly used in SMT-COMP. The difficulty is measured by the complexity of the composition (\n                    <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n                    ., number of variables, clauses) and the interdependencies within constraints. Grater again solves the same number of constraints as Bitwuzla and CVC5 while running over 10 times faster than both solvers in average solving time, and over 50 times (\n                    <jats:italic toggle=\"yes\">resp<\/jats:italic>\n                    . 30 times) faster than Bitwuzla (\n                    <jats:italic toggle=\"yes\">resp<\/jats:italic>\n                    . CVC5) in median solving time.\n                  <\/jats:p>\n                  <jats:p>\n                    We release the source code of Grater, along with all evaluation data, including detailed comparisons of Grater against each baseline solver (\n                    <jats:italic toggle=\"yes\">i.e<\/jats:italic>\n                    ., Z3, CVC5, Bitwuzla, JFS, XSat, and CoverMe), at\n                    <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/github.com\/grater-exp\/grater-experiment\">https:\/\/github.com\/grater-exp\/grater-experiment<\/jats:ext-link>\n                    to facilitate reproducibility.\n                  <\/jats:p>","DOI":"10.1145\/3729279","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"725-747","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Solving Floating-Point Constraints with Continuous Optimization"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-0312-0571","authenticated-orcid":false,"given":"Qian","family":"Chen","sequence":"first","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0696-6975","authenticated-orcid":false,"given":"Chenqi","family":"Cui","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8185-0573","authenticated-orcid":false,"given":"Fengjuan","family":"Gao","sequence":"additional","affiliation":[{"name":"Nanjing University of Science and Technology, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7216-6929","authenticated-orcid":false,"given":"Yu","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0844-5023","authenticated-orcid":false,"given":"Ke","family":"Wang","sequence":"additional","affiliation":[{"name":"Visa Research, Palo Alto, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4794-1652","authenticated-orcid":false,"given":"Linzhang","family":"Wang","sequence":"additional","affiliation":[{"name":"Nanjing University, Nanjing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1966.16.1"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Roberto Bagnara Matthieu Carlier Roberta Gori and Arnaud Gotlieb. 2013. Symbolic Path-Oriented Test Data Generation for Floating-Point Programs. In 2013 IEEE Sixth International Conference on Software Testing Verification and Validation. 1\u201310. doi:10.1109\/ICST.2013.17","DOI":"10.1109\/ICST.2013.17"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_5_1","doi-asserted-by":"crossref","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. Handbook of model checking (2018) 305\u2013343.","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_18"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_22"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Mateus Borges Marcelo d\u2019Amorim Saswat Anand David Bushnell and Corina S. Pasareanu. 2012. Symbolic Execution with Interval Solving and Meta-heuristic Search. In 2012 IEEE Fifth International Conference on Software Testing Verification and Validation. 111\u2013120. doi:10.1109\/ICST.2012.91","DOI":"10.1109\/ICST.2012.91"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-005-9004-z"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008820505350"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00538-3"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3641289"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1137\/0720013"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_16_1","first-page":"244","article-title":"Lemmas on demand for satisfiability solvers","volume":"2","author":"De Moura Leonardo","year":"2002","unstructured":"Leonardo De Moura, Harald Rue\u00df, and Maria Sorea. 2002. Lemmas on demand for satisfiability solvers. Proc. SAT 2 (2002), 244\u2013251.","journal-title":"Proc. SAT"},{"key":"e_1_3_2_17_1","volume-title":"Constraint processing","author":"Dechter Rina","year":"2003","unstructured":"Rina Dechter. 2003. Constraint processing. Morgan Kaufmann."},{"key":"e_1_3_2_18_1","first-page":"187","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 28","author":"Fu Zhoulai","year":"2016","unstructured":"Zhoulai Fu and Zhendong Su. 2016. XSat: a fast floating-point satisfiability solver. In Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 28. Springer, 187\u2013209."},{"key":"e_1_3_2_19_1","doi-asserted-by":"crossref","unstructured":"Zhoulai Fu and Zhendong Su. 2017. Achieving high coverage for floating-point code via unconstrained programming. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 306\u2013319.","DOI":"10.1145\/3062341.3062383"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314632"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"e_1_3_2_23_1","first-page":"1724","volume-title":"Proceedings of the 34th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 70)","author":"Jin Chi","year":"2017","unstructured":"Chi Jin, Rong Ge, Praneeth Netrapalli, Sham M. Kakade, and Michael I. Jordan. 2017. How to Escape Saddle Points Efficiently. In Proceedings of the 34th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 70), Doina Precup and Yee Whye Teh (Eds.). PMLR, 1724\u20131732. https:\/\/proceedings.mlr.press\/v70\/jin17a.html"},{"issue":"94720","key":"e_1_3_2_24_1","first-page":"11","article-title":"IEEE standard 754 for binary floating-point arithmetic","volume":"754","author":"Kahan William","year":"1996","unstructured":"William Kahan. 1996. IEEE standard 754 for binary floating-point arithmetic. Lecture Notes on the Status of IEEE 754, 94720-1776 (1996), 11.","journal-title":"Lecture Notes on the Status of IEEE"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102235"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16573-3_11"},{"key":"e_1_3_2_27_1","unstructured":"Florian Lapschies Jan Peleska Elena Gorbachuk and Tatiana Mangels. 2012. Sonolar SMT-solver. Satisfiability modulo theories competition; system description (2012)."},{"key":"e_1_3_2_28_1","first-page":"1","volume-title":"2014 Design, Automation & Test in Europe Conference & Exhibition (DATE)","author":"Leeser Miriam","year":"2014","unstructured":"Miriam Leeser, Saoni Mukherjee, Jaideep Ramachandran, and Thomas Wahl. 2014. Make it real: Effective floating-point reasoning via exact arithmetic. In 2014 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 1\u20134."},{"key":"e_1_3_2_29_1","doi-asserted-by":"crossref","unstructured":"Xin Li Yongjuan Liang Hong Qian Yi-Qi Hu Lei Bu Yang Yu Xin Chen and Xuandong Li. 2016. Symbolic execution of complex program driven by machine learning based constraint solving. In Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering. 554\u2013559.","DOI":"10.1145\/2970276.2970364"},{"key":"e_1_3_2_30_1","doi-asserted-by":"crossref","unstructured":"Daniel Liew Cristian Cadar Alastair F Donaldson and J Ryan Stinnett. 2019. Just fuzz it: solving floating-point constraints using coverage-guided fuzzing. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 521\u2013532.","DOI":"10.1145\/3338906.3338921"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02289146"},{"key":"e_1_3_2_32_1","unstructured":"Bruno Marre Fran\u00e7ois Bobot and Zakaria Chihani. 2017. Real behavior of floating point numbers. In The SMT Workshop."},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45578-7_36"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_36_1","first-page":"1","volume-title":"Numerical optimization","author":"Nocedal Jorge","year":"2006","unstructured":"Jorge Nocedal and Stephen J. Wright. 2006. Numerical optimization. Springer Nature, 1\u2013664."},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4145-2"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_26"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45757-7_26"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41592-019-0686-2"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1038\/30918"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v30i1.10289"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:09:19Z","timestamp":1784196559000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":41,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729279"],"URL":"https:\/\/doi.org\/10.1145\/3729279","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}