{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:56:23Z","timestamp":1781884583419,"version":"3.54.5"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on\n                    <jats:italic>single cell construction<\/jats:italic>\n                    , the task of generalizing a sample point to a connected subset (cell) of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mathbb {R}^n$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>R<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mi>n<\/mml:mi>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , that contains the sample and over which a given set of polynomials is sign-invariant.\n                  <\/jats:p>\n                  <jats:p>In this paper, we propose to speed up the computation and simplify the representation of the resulting cell by dynamically extending the considered set of polynomials with further linear polynomials. While this increases the total number of (smaller) cells generated throughout the algorithm, our experiments show that it can pay off when using suitable heuristics due to the interaction with Boolean reasoning.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_7","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:40Z","timestamp":1753789660000},"page":"116-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["More is Less: Adding Polynomials for\u00a0Faster Explanations in\u00a0NLSAT"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3086-9976","authenticated-orcid":false,"given":"Valentin","family":"Promies","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2641-1380","authenticated-orcid":false,"given":"Jasper","family":"Nalbach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5647-6134","authenticated-orcid":false,"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2020.100633","volume":"119","author":"E \u00c1brah\u00e1m","year":"2021","unstructured":"\u00c1brah\u00e1m, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program. 119, 100633 (2021). https:\/\/doi.org\/10.1016\/J.JLAMP.2020.100633","journal-title":"J. Log. Algebraic Methods Program."},{"key":"7_CR2","unstructured":"\u00c1brah\u00e1m, E., Nalbach, J., Kremer, G.: Embedding the virtual substitution method in the model constructing satisfiability calculus framework. In: England, M., Ganesh, V. (eds.) Proc. of SC$$ ^2$$\u201917. CEUR Workshop Proceedings, vol.\u00a01974. CEUR-WS.org (2017), https:\/\/ceur-ws.org\/Vol-1974\/EAb.pdf"},{"key":"7_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard \u2013 version 2.0. In: Proc. of SMT \u201910 (2010), http:\/\/theory.stanford.edu\/~barrett\/pubs\/BST10.pdf"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability Modulo Theories, pp. 305\u2013343. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bj\u00f8rner, N.S., Sofronie-Stokkermans, V. (eds.) Proc. of CADE\u201911. LNCS, vol.\u00a06803, pp. 116\u2013130. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11, https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M., M\u00fcller, N.: A cdcl-style calculus for solving non-linear constraints. In: Herzig, A., Popescu, A. (eds.) Frontiers of Combining Systems. pp. 131\u2013148. Springer (2019)","DOI":"10.1007\/978-3-030-29007-8_8"},{"key":"7_CR7","unstructured":"Brocot, A.: Calcul des rouages par approximation: Nouvelle m\u00e9thode. Revue chronom\u00e9trique. Journal des horlogers, scientifique et pratique 3, 186\u2013194 (1861), https:\/\/gallica.bnf.fr\/ark:\/12148\/bpt6k1661912"},{"issue":"5","key":"7_CR8","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1006\/JSCO.2001.0463","volume":"32","author":"CW Brown","year":"2001","unstructured":"Brown, C.W.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput. 32(5), 447\u2013465 (2001). https:\/\/doi.org\/10.1006\/JSCO.2001.0463","journal-title":"J. Symb. Comput."},{"key":"7_CR9","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/J.JSC.2014.09.024","volume":"70","author":"CW Brown","year":"2015","unstructured":"Brown, C.W., Ko\u0161ta, M.: Constructing a single cell in cylindrical algebraic decomposition. J. Symb. Comput. 70, 14\u201348 (2015). https:\/\/doi.org\/10.1016\/J.JSC.2014.09.024","journal-title":"J. Symb. Comput."},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1\u201319:52 (2018). https:\/\/doi.org\/10.1145\/3230639, https:\/\/doi.org\/10.1145\/3230639","DOI":"10.1145\/3230639"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Automata Theory and Formal Languages, 2nd GI Conference, Kaiserslautern, May 20-23, 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17","DOI":"10.1007\/3-540-07407-4_17"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: An open source C++ toolbox for strategic and parallel SMT solving. In: Proc. of SAT\u201915. LNCS, vol.\u00a09340, pp. 360\u2013368. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Ideals, varieties, and algorithms - an introduction to computational algebraic geometry and commutative algebra (2. ed.). Undergraduate texts in mathematics, Springer (1997). https:\/\/doi.org\/10.1007\/978-3-662-41154-4","DOI":"10.1007\/978-3-662-41154-4"},{"key":"7_CR14","unstructured":"cvc5: An efficient open-source automatic theorem prover for satisfiability modulo theories (smt) problems., https:\/\/cvc5.github.io\/"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Gutierrez, J. (ed.) Proc. of ISSAC\u201904. pp. 111\u2013118. ACM (2004). https:\/\/doi.org\/10.1145\/1005285.1005303, https:\/\/doi.org\/10.1145\/1005285.1005303","DOI":"10.1145\/1005285.1005303"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dreal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) Proc. of CADE\u201913. LNCS, vol.\u00a07898, pp. 208\u2013214. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with aprove. J. Autom. Reason. 58(1), 3\u201331 (2017). https:\/\/doi.org\/10.1007\/S10817-016-9388-Y, https:\/\/doi.org\/10.1007\/s10817-016-9388-y","DOI":"10.1007\/S10817-016-9388-Y"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Barrett, C., de\u00a0Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Proc. of FMCAD\u201913. pp. 173\u2013180 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.7027033","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., de\u00a0Moura, L.M.: Solving non-linear arithmetic. In: Proc. of IJCAR\u201912. LNCS, vol.\u00a07364, pp. 339\u2013354. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"7_CR20","unstructured":"Kremer, G.: Cylindrical algebraic decomposition for nonlinear arithmetic problems. Ph.D. thesis, RWTH Aachen University, Germany (2020), https:\/\/publications.rwth-aachen.de\/record\/792185"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Lazard, D.: An Improved Projection for Cylindrical Algebraic Decomposition, pp. 467\u2013476. Springer (1994). https:\/\/doi.org\/10.1007\/978-1-4612-2628-4_29","DOI":"10.1007\/978-1-4612-2628-4_29"},{"key":"7_CR22","unstructured":"Li, H., Xia, B.: Solving satisfiability of polynomial formulas by sample-cell projection. CoRR abs\/2003.00409 (2020), https:\/\/arxiv.org\/abs\/2003.00409"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B.F. (ed.) Proc. of EUROCAL\u201985. LNCS, vol.\u00a0204, pp. 277\u2013278. Springer (1985). https:\/\/doi.org\/10.1007\/3-540-15984-3_277","DOI":"10.1007\/3-540-15984-3_277"},{"key":"7_CR24","doi-asserted-by":"publisher","unstructured":"McCallum, S.: On projection in cad-based quantifier elimination with equational constraint. In: Geddes, K.O., Salvy, B., Dooley, S.S. (eds.) Proc. of ISSAC \u201999. pp. 145\u2013149. ACM (1999). https:\/\/doi.org\/10.1145\/309831.309892","DOI":"10.1145\/309831.309892"},{"key":"7_CR25","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Jovanovic, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Proc of VMCAI\u201913. LNCS, vol.\u00a07737, pp. 1\u201312. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Nalbach, J., \u00c1brah\u00e1m, E.: Merging adjacent cells during single cell construction. In: Boulier, F., Mou, C., Sadykov, T.M., Vorozhtsov, E.V. (eds.) Proc. of CASC\u201924. LNCS, vol. 14938, pp. 252\u2013272. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-69070-9_15, https:\/\/doi.org\/10.1007\/978-3-031-69070-9_15","DOI":"10.1007\/978-3-031-69070-9_15"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Nalbach, J., Kremer, G.: Extensions of the cylindrical algebraic covering method for quantifiers. CoRR abs\/2411.03070 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2411.03070, https:\/\/doi.org\/10.48550\/arXiv.2411.03070","DOI":"10.48550\/ARXIV.2411.03070"},{"key":"7_CR28","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2023.102288","volume":"123","author":"J Nalbach","year":"2024","unstructured":"Nalbach, J., \u00c1brah\u00e1m, E., Specht, P., Brown, C.W., Davenport, J.H., England, M.: Levelwise construction of a single cylindrical algebraic cell. J. Symb. Comput. 123, 102288 (2024). https:\/\/doi.org\/10.1016\/j.jsc.2023.102288","journal-title":"J. Symb. Comput."},{"key":"7_CR29","unstructured":"Promies, V., Nalbach, J., \u00c1brah\u00e1m, E.: Under-approximation of a single algebraic cell (extended abstract). In: Brown, C.W., Kaufmann, D., Nalon, C., Steen, A., Suda, M. (eds.) Proc. of IJCAR\u201924. CEUR Workshop Proceedings, vol.\u00a03717, pp. 132\u2013136. CEUR-WS.org (2024), https:\/\/ceur-ws.org\/Vol-3717\/short3.pdf"},{"key":"7_CR30","unstructured":"SMT-RAT, a toolbox for strategic and parallel satisfiability modulo theories solving, https:\/\/github.com\/ths-rwth\/smtrat"},{"issue":"55","key":"7_CR31","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1515\/crll.1858.55.193","volume":"1858","author":"M Stern","year":"1858","unstructured":"Stern, M.: Ueber eine zahlentheoretische Funktion. Journal f\u00fcr die reine und angewandte Mathematik (Crelles Journal) 1858(55), 193\u2013220 (1858). https:\/\/doi.org\/10.1515\/crll.1858.55.193","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik (Crelles Journal)"},{"issue":"5","key":"7_CR32","doi-asserted-by":"publisher","first-page":"1340","DOI":"10.1109\/TAC.2015.2465212","volume":"61","author":"J Xu","year":"2016","unstructured":"Xu, J., Van Den Boom, T., De Schutter, B., Luo, X.L.: Minimal Conjunctive Normal Expression of Continuous Piecewise Affine Functions. IEEE Trans. Autom. Control 61(5), 1340\u20131345 (2016). https:\/\/doi.org\/10.1109\/TAC.2015.2465212","journal-title":"IEEE Trans. Autom. Control"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Xu, J., van den Boom, T.J., De\u00a0Schutter, B.: Irredundant lattice piecewise affine representations and their applications in explicit model predictive control. In: Decision and Control (CDC 2014). pp. 4416\u20134421. IEEE (Dec 2014). https:\/\/doi.org\/10.1109\/CDC.2014.7040078","DOI":"10.1109\/CDC.2014.7040078"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:27:14Z","timestamp":1781882834000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}