{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:22:59Z","timestamp":1762816979178,"version":"build-2065373602"},"publisher-location":"Singapore","reference-count":13,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819542123"},{"type":"electronic","value":"9789819542130"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-4213-0_18","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:17:51Z","timestamp":1762816671000},"page":"329-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Avoiding Larger Conflict Regions in\u00a0CDCL-Style Methods for\u00a0Solving SMT-NRA"],"prefix":"10.1007","author":[{"given":"Xinpeng","family":"Ni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tianyi","family":"Ding","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"issue":"5","key":"18_CR1","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)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"18_CR2","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM Sigsam Bull. 37(4), 97\u2013108 (2003)","journal-title":"ACM Sigsam Bull."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Brown, C.W.: Constructing a single open cell in a cylindrical algebraic decomposition. In: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, pp. 133\u2013140 (2013)","DOI":"10.1145\/2465506.2465952"},{"issue":"1","key":"18_CR4","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1093390.1093393","volume":"10","author":"GE Collins","year":"1976","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. ACM SIGSAM Bull. 10(1), 10\u201312 (1976)","journal-title":"ACM SIGSAM Bull."},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, pp. 261\u2013264 (1990)","DOI":"10.1145\/96877.96943"},{"key":"18_CR7","unstructured":"Li, H., Xia, B.: Solving Satisfiability of Polynomial Formulas by Sample-Cell Projection. arXiv preprint arXiv:2003.00409 (2020)"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, LNCS, pp. 242\u2013268. Springer, Vienna (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_12","DOI":"10.1007\/978-3-7091-9459-1_12"},{"key":"18_CR9","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.) Computer Algebra in Scientific Computing. CASC 2024. LNCS, vol. 14938, pp. 252\u2013272. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-69070-9_15","DOI":"10.1007\/978-3-031-69070-9_15"},{"key":"18_CR10","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)","journal-title":"J. Symb. Comput."},{"issue":"3\u20134","key":"18_CR11","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3\u20134), 141\u2013224 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"3","key":"18_CR12","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1006\/jsco.1999.0327","volume":"29","author":"A Strzebo\u0144ski","year":"2000","unstructured":"Strzebo\u0144ski, A.: Solving systems of strict polynomial inequalities. J. Symb. Comput. 29(3), 471\u2013480 (2000)","journal-title":"J. Symb. Comput."},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: Caviness, B.F., Johnson, J.R. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, LNCS, pp. 24\u201384. Springer, Vienna (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_3","DOI":"10.1007\/978-3-7091-9459-1_3"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:18:12Z","timestamp":1762816692000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","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":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}