{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:00Z","timestamp":1776333420030,"version":"3.51.2"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"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><jats:p>We introduce a novel variable elimination method for <jats:italic>conjunctions<\/jats:italic> of <jats:italic>linear<\/jats:italic> real arithmetic constraints. In prior work, we derived a variant of the Fourier-Motzkin elimination, which uses case splitting to reduce the procedure\u2019s complexity from doubly to singly exponential. This variant, which we call FMplex, was originally developed for satisfiability checking, and it essentially performs a depth-first search in a tree of sub-problems. It can be adapted straightforwardly for the task of quantifier elimination, but it returns <jats:italic>disjunctions<\/jats:italic> of conjunctions, even though the solution space can always be defined by a single conjunction. Our main contribution is to show how to efficiently extract an equivalent <jats:italic>conjunction<\/jats:italic> from the search tree. Besides the theoretical foundations, we explain how the procedure relates to other methods for quantifier elimination and polyhedron projection. An experimental evaluation demonstrates that our implementation is competitive with established tools.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_7","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"131-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Divide-and-Conquer Approach to\u00a0Variable Elimination in\u00a0Linear Real Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3086-9976","authenticated-orcid":false,"given":"Valentin","family":"Promies","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5647-6134","authenticated-orcid":false,"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Antal, L., Masara, H., \u00c1brah\u00e1m, E.: Extending neural network verification to a larger family of piece-wise linear activation functions. In: Proceedings of the 5th International Workshop on Formal Methods for Autonomous Systems (FMAS@iFM\u201923). EPTCS, vol.\u00a0395, pp. 30\u201368 (2023). https:\/\/doi.org\/10.4204\/EPTCS.395.4","DOI":"10.4204\/EPTCS.395.4"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008). https:\/\/doi.org\/10.1016\/J.SCICO.2007.08.001","DOI":"10.1016\/J.SCICO.2007.08.001"},{"key":"7_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Janota, M.: Playing with quantified satisfaction. In: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, (LPAR 2015). EPiC Series in Computing, vol.\u00a035, pp. 15\u201327. EasyChair (2015). https:\/\/doi.org\/10.29007\/VV21","DOI":"10.29007\/VV21"},{"key":"7_CR5","unstructured":"CDDlib. Commit aff2477. https:\/\/github.com\/cddlib\/cddlib\/tree\/aff2477f8ab25e826da93c6650731dd1717d6b4a"},{"issue":"5","key":"7_CR6","first-page":"1075","volume":"152","author":"SN Chernikov","year":"1963","unstructured":"Chernikov, S.N.: Contraction of systems of linear inequalities. Dokl. Akad. Nauk SSSR 152(5), 1075\u20131078 (1963)","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"7_CR7","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: Heule, M., Weaver, S. (eds.) SAT 2015, pp. 360\u2013368. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26","DOI":"10.1007\/978-3-319-24318-4_26"},{"issue":"2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2\u20139 (1997). https:\/\/doi.org\/10.1145\/261320.261324","journal-title":"ACM SIGSAM Bull."},{"issue":"124","key":"7_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1515\/crll.1902.124.1","volume":"1902","author":"J Farkas","year":"1902","unstructured":"Farkas, J.: Theorie der einfachen Ungleichungen. J. f\u00fcr die reine und angewandte Mathematik (Crelles J.) 1902(124), 1\u201327 (1902). https:\/\/doi.org\/10.1515\/crll.1902.124.1","journal-title":"J. f\u00fcr die reine und angewandte Mathematik (Crelles J.)"},{"key":"7_CR10","unstructured":"Fourier, J.B.J.: Analyse des travaux de l\u2019Acad\u00e9mie Royale des Sciences pendant l\u2019ann\u00e9e 1824. Partie Math\u00e9matique (1827)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-61576-8_77","volume-title":"Combinatorics and Computer Science","author":"K Fukuda","year":"1996","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Deza, M., Euler, R., Manoussakis, I. (eds.) CCS 1995. LNCS, vol. 1120, pp. 91\u2013111. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61576-8_77"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with approve. J. Autom. Reason. 58(1), 3\u201331 (2017). https:\/\/doi.org\/10.1007\/S10817-016-9388-Y","DOI":"10.1007\/S10817-016-9388-Y"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kuncak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"7_CR14","unstructured":"Imbert, J.: Fourier\u2019s elimination: which to choose? In: Proceedings of the 2nd Workshop on Principles and Practice of Constraint Programming (PPCP 1993), pp. 117\u2013129 (1993)"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Min\u00e9, A.: APRON: a library of numerical abstract domains for static analysis. In: CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Jing, R., Maza, M.M., Talaashrafi, D.: Complexity estimates for Fourier-Motzkin elimination. In: CASC 2020. LNCS, vol. 12291, pp. 282\u2013306. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-60026-6_16","DOI":"10.1007\/978-3-030-60026-6_16"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Jones, C., Kerrigan, E., Maciejowski, J.M.: On polyhedral projection and parametric programming. J. Optimiz. Theory Appl. 138, 207\u2013220 (2008). https:\/\/doi.org\/10.1007\/s10957-008-9384-4","DOI":"10.1007\/s10957-008-9384-4"},{"issue":"3","key":"7_CR18","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"KD Julian","year":"2019","unstructured":"Julian, K.D., Kochenderfer, M.J., Owen, M.P.: Deep neural network compression for aircraft collision avoidance systems. J. Guid. Control. Dyn. 42(3), 598\u2013608 (2019). https:\/\/doi.org\/10.2514\/1.G003724","journal-title":"J. Guid. Control. Dyn."},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Korovin, K., Kosta, M., Sturm, T.: Towards conflict-driven learning for virtual substitution. In: CASC 2014. LNCS, vol.\u00a08660, pp. 256\u2013270. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-10515-4_19","DOI":"10.1007\/978-3-319-10515-4_19"},{"key":"7_CR20","unstructured":"Kos\u0306ta, M.: New Concepts for Real Quantifier Elimination by Virtual Substitution. Ph.D. thesis, Universit\u00e4t des Saarlandes, Germany (2016). http:\/\/dx.doi.org\/10.22028\/D291-26679"},{"issue":"5","key":"7_CR21","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/COMJNL\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993). https:\/\/doi.org\/10.1093\/COMJNL\/36.5.450","journal-title":"Comput. J."},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008). LNCS, vol.\u00a05330, pp. 243\u2013257. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_18","DOI":"10.1007\/978-3-540-89439-1_18"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The Double Description Method, pp. 51\u201374. Princeton University Press, Princeton (1953). https:\/\/doi.org\/10.1515\/9781400881970-004","DOI":"10.1515\/9781400881970-004"},{"key":"7_CR24","volume-title":"Beitr\u00e4ge zur Theorie der linearen Ungleichungen (Dissertation)","author":"TS Motzkin","year":"1936","unstructured":"Motzkin, T.S.: Beitr\u00e4ge zur Theorie der linearen Ungleichungen (Dissertation). Buchdr\u00fcckeri Azriel, Jerusalem (1936)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"9","key":"7_CR26","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"LM de Moura","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011). https:\/\/doi.org\/10.1145\/1995376.1995394","journal-title":"Commun. ACM"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Nalbach, J., Promies, V., \u00c1brah\u00e1m, E., Kobialka, P.: FMplex: a novel method for solving linear real arithmetic problems. In: Proceedings of the 14th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2023). EPTCS, vol.\u00a0390, pp. 16\u201332 (2023). https:\/\/doi.org\/10.4204\/EPTCS.390.2","DOI":"10.4204\/EPTCS.390.2"},{"key":"7_CR28","unstructured":"Reduce, Snapshot 2023-03-08. https:\/\/sourceforge.net\/projects\/reduce-algebra\/files\/snapshot_2023-03-08\/linux64\/reduce-complete_6547_amd64.deb"},{"key":"7_CR29","unstructured":"SMT-RAT, a toolbox for strategic and parallel Satisfiability Modulo Theories solving. https:\/\/github.com\/ths-rwth\/smtrat\/tree\/pub\/fmplex-qe-3"},{"key":"7_CR30","doi-asserted-by":"publisher","unstructured":"Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-030-32304-2_11","volume-title":"Static Analysis","author":"H Yu","year":"2019","unstructured":"Yu, H., Monniaux, D.: An efficient parametric linear programming solver and application to polyhedral projection. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 203\u2013224. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_11"},{"key":"7_CR32","unstructured":"z3 theorem prover, commit 520e692. https:\/\/github.com\/Z3Prover\/z3\/tree\/520e692a43c41e8981eb091494bef0297ecbe3c6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:03:33Z","timestamp":1725933813000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","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":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}