{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T02:49:30Z","timestamp":1768790970535,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2025-07159"],"award-info":[{"award-number":["RGPIN-2025-07159"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,7,28]]},"DOI":"10.1145\/3747199.3747580","type":"proceedings-article","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T10:51:17Z","timestamp":1762771877000},"page":"353-362","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantifier Elimination Over the Integers"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6932-8862","authenticated-orcid":false,"given":"Rui-Juan","family":"Jing","sequence":"first","affiliation":[{"name":"Jinagsu University, Zhenjiang, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7010-7932","authenticated-orcid":false,"given":"Yuzhuo","family":"Lei","sequence":"additional","affiliation":[{"name":"Ontario Research Center for Computer Algebra, University of Western Ontario, London, ON, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2240-4647","authenticated-orcid":false,"given":"Christopher Frank Stephan","family":"Maligec","sequence":"additional","affiliation":[{"name":"Ontario Research Center for Computer Algebra, University of Western Ontario, London, ON, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3011-0756","authenticated-orcid":false,"given":"Marc","family":"Moreno Maza","sequence":"additional","affiliation":[{"name":"Computer Science, Ontario Research Center for Computer Algebra, University of Western Ontario, London Ontario, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6692-3305","authenticated-orcid":false,"given":"Chirantan","family":"Mukherjee","sequence":"additional","affiliation":[{"name":"Ontario Research Center for Computer Algebra, University of Western Ontario, London, ON, Canada"}]}],"member":"320","published-online":{"date-parts":[[2025,11,10]]},"reference":[{"key":"e_1_3_3_3_2_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_3_3_3_3_2","doi-asserted-by":"crossref","unstructured":"Alexander Barvinok and James\u00a0E Pommersheim. 1999. An algorithmic theory of lattice points in polyhedra. New perspectives in algebraic combinatorics 38 (1999) 91\u2013147.","DOI":"10.1017\/9781009701587.004"},{"key":"e_1_3_3_3_4_2","doi-asserted-by":"crossref","unstructured":"Alexander\u00a0I. Barvinok. 1994. A Polynomial Time Algorithm for Counting Integral Points in Polyhedra When the Dimension is Fixed. Math. Oper. Res. 19 4 (1994) 769\u2013779.","DOI":"10.1287\/moor.19.4.769"},{"key":"e_1_3_3_3_5_2","doi-asserted-by":"publisher","unstructured":"Saugata Basu Richard Pollack and Marie-Franccoise Roy. 1996. On the Combinatorial and Algebraic Complexity of Quantifier Elimination. J. ACM 43 6 (1996) 1002\u20131045. 10.1145\/235809.235813","DOI":"10.1145\/235809.235813"},{"key":"e_1_3_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611976496.3"},{"key":"e_1_3_3_3_7_2","doi-asserted-by":"publisher","unstructured":"Tristram Bogart John Goodrick and Kevin Woods. 2017. Parametric Presburger arithmetic: logic combinatorics and quasi-polynomial behavior. Discrete Analysis (jan 16 2017). 10.19086\/da.1254","DOI":"10.19086\/da.1254"},{"key":"e_1_3_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1277548.1277557"},{"key":"e_1_3_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_12"},{"key":"e_1_3_3_3_10_2","unstructured":"David\u00a0C Cooper. 1972. Theorem proving in arithmetic without multiplication. Machine intelligence 7 91-99 (1972) 300."},{"key":"e_1_3_3_3_11_2","doi-asserted-by":"crossref","unstructured":"Friedrich Eisenbrand and Gennady Shmonin. 2008. Parametric Integer Programming in Fixed Dimension. Math. Oper. Res. 33 4 (2008) 839\u2013850.","DOI":"10.1287\/moor.1080.0320"},{"key":"e_1_3_3_3_12_2","doi-asserted-by":"crossref","unstructured":"P. Feautrier. 1988. Parametric integer programming. RAIRO. Recherche op\u00e9rationnelle 22 3 (1988) 243 \u2013 268.","DOI":"10.1051\/ro\/1988220302431"},{"key":"e_1_3_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2751205.2751248"},{"key":"e_1_3_3_3_14_2","doi-asserted-by":"crossref","unstructured":"Christoph Haase. 2018. A survival guide to Presburger arithmetic. ACM SIGLOG News 5 3 (2018) 67\u201382.","DOI":"10.1145\/3242953.3242964"},{"key":"e_1_3_3_3_15_2","series-title":"LIPIcs","first-page":"142:1\u2013142:17","volume-title":"ICALP 2024a","author":"Haase Christoph","year":"2024","unstructured":"Christoph Haase, Shankara\u00a0Narayanan Krishna, Khushraj Madnani, Om\u00a0Swostik Mishra, and Georg Zetzsche. 2024. An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. In ICALP 2024a(LIPIcs, Vol.\u00a0297). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 142:1\u2013142:17."},{"key":"e_1_3_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-69070-9_9"},{"key":"e_1_3_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66320-3_17"},{"key":"e_1_3_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66320-3_18"},{"key":"e_1_3_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3666000.3669708"},{"key":"e_1_3_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-74759-0_187"},{"key":"e_1_3_3_3_21_2","unstructured":"Oliver Knill. 2012. A Multivariable Chinese Remainder Theorem. arxiv:https:\/\/arXiv.org\/abs\/1206.5114\u00a0[math.HO] https:\/\/arxiv.org\/abs\/1206.5114"},{"key":"e_1_3_3_3_22_2","volume-title":"An Implementation of the Barvinok\u2013Woods Integer Projection Algorithm","author":"K\u00f6ppe Matthias","year":"2008","unstructured":"Matthias K\u00f6ppe, Sven Verdoolaege, and Kevin\u00a0M. Woods. 2008. An Implementation of the Barvinok\u2013Woods Integer Projection Algorithm. Technical Report. Oberlin College, Department of Mathematics."},{"key":"e_1_3_3_3_23_2","unstructured":"Catherine Lassez. 1992. Quantifier elimination for conjunctions of linear constraints via a convex hull algorithm. Symbolic and Numerical Computation for Artificial Intelligence (1992) 103\u2013122."},{"key":"e_1_3_3_3_24_2","doi-asserted-by":"crossref","unstructured":"Jean-Louis Lassez and Michael\u00a0J Maher. 1992. On Fourier\u2019s algorithm for linear arithmetic constraints. Journal of Automated Reasoning 9 (1992) 373\u2013379.","DOI":"10.1007\/BF00245296"},{"key":"e_1_3_3_3_25_2","doi-asserted-by":"crossref","unstructured":"Jes\u00fas A.\u00a0De Loera Raymond Hemmecke Jeremiah Tauzer and Ruriko Yoshida. 2004. Effective lattice point counting in rational convex polytopes. J. Symb. Comput. 38 4 (2004) 1273\u20131302.","DOI":"10.1016\/j.jsc.2003.04.003"},{"key":"e_1_3_3_3_26_2","doi-asserted-by":"crossref","unstructured":"Vadim Maslov. 1992. Delinearization: An efficient way to break multiloop dependence equations. ACM Sigplan Notices 27 7 (1992) 152\u2013161.","DOI":"10.1145\/143103.143130"},{"key":"e_1_3_3_3_27_2","series-title":"LNCS","first-page":"252","volume-title":"CASC 2021, Proceedings","volume":"12865","author":"Maza Marc Moreno","year":"2021","unstructured":"Marc Moreno Maza and Linxiao Wang. 2021. On the Pseudo-Periodicity of the Integer Hull of Parametric Convex Polygons. In CASC 2021, Proceedings(LNCS, Vol.\u00a012865). Springer, 252\u2013271."},{"key":"e_1_3_3_3_28_2","doi-asserted-by":"crossref","unstructured":"William Pugh. 1992. A Practical Algorithm for Exact Array Dependence Analysis. Commun. ACM 35 8 (1992) 102\u2013114.","DOI":"10.1145\/135226.135233"},{"key":"e_1_3_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"key":"e_1_3_3_3_30_2","doi-asserted-by":"crossref","unstructured":"Arvind Rajan. 1990. Theory of linear and integer programming by Alexander Schrijver Wiley New York 1986 471 pp. Price $71.95. Networks 20 6 (1990) 801.","DOI":"10.1002\/net.3230200608"},{"key":"e_1_3_3_3_31_2","volume-title":"Theory of linear and integer programming","author":"Schrijver Alexander","year":"1999","unstructured":"Alexander Schrijver. 1999. Theory of linear and integer programming. Wiley."},{"key":"e_1_3_3_3_32_2","doi-asserted-by":"crossref","unstructured":"Rachid Seghir Vincent Loechner and Benoit Meister. 2012. Integer affine transformations of parametric \\(\\mathbb {Z}\\)-polytopes and applications to loop nest optimization. ACM Trans. Archit. Code Optim. 9 2 (2012) 8:1\u20138:27.","DOI":"10.1145\/2207222.2207224"},{"key":"e_1_3_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/867696"},{"key":"e_1_3_3_3_34_2","unstructured":"Arne Storjohann. 2000. Algorithms for matrix canonical forms. Ph.\u00a0D. Dissertation. Swiss Federal Institute of Technology Zurich."},{"key":"e_1_3_3_3_35_2","unstructured":"Thomas Sturm. 2023. Algorithmic Quantifier Elimination. Lecture Notes. https:\/\/www.mpi-inf.mpg.de\/fileadmin\/inf\/rg1\/Documents\/2023-07-14-lnqe.pdf Accessed: 2025-04-17."},{"key":"e_1_3_3_3_36_2","doi-asserted-by":"crossref","unstructured":"B Sury. 2015. Multivariable Chinese remainder theorem. Resonance 20 (2015) 206\u2013216.","DOI":"10.1007\/s12045-015-0171-x"},{"key":"e_1_3_3_3_37_2","volume-title":"International Workshop on Polyhedral Compilation Techniques, Date: 2015\/01\/19-2015\/01\/19, Location: Amsterdam, The Netherlands","author":"Verdoolaege Sven","year":"2015","unstructured":"Sven Verdoolaege. 2015. Integer set coalescing. In International Workshop on Polyhedral Compilation Techniques, Date: 2015\/01\/19-2015\/01\/19, Location: Amsterdam, The Netherlands."},{"key":"e_1_3_3_3_38_2","unstructured":"S. Verdoolaege. 2024. Integer Set Library: Manual Version: isl-0.27. 288\u00a0pages. https:\/\/libisl.sourceforge.io\/manual.pdf"},{"key":"e_1_3_3_3_39_2","doi-asserted-by":"crossref","unstructured":"Sven Verdoolaege Rachid Seghir Kristof Beyls Vincent Loechner and Maurice Bruynooghe. 2007. Counting Integer Points in Parametric Polytopes Using Barvinok\u2019s Rational Functions. Algorithmica 48 1 (2007) 37\u201366.","DOI":"10.1007\/s00453-006-1231-0"},{"key":"e_1_3_3_3_40_2","doi-asserted-by":"crossref","unstructured":"H.P. Williams and J.N. Hooker. 2016. Integer programming as projection. Discrete Optimization 22 (2016) 291\u2013311.","DOI":"10.1016\/j.disopt.2016.08.004"},{"key":"e_1_3_3_3_41_2","doi-asserted-by":"crossref","unstructured":"H\u00a0Paul Williams. 1976. Fourier-Motzkin elimination extension to integer programming problems. Journal of combinatorial theory series A 21 1 (1976) 118\u2013123.","DOI":"10.1016\/0097-3165(76)90055-8"}],"event":{"name":"ISSAC '25: International Symposium on Symbolic and Algebraic Computation","location":"Guanajuato Mexico","acronym":"ISSAC '25","sponsor":["SIGSAM ACM Special Interest Group on Symbolic and Algebraic Manipulation"]},"container-title":["Proceedings of the 2025 International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747199.3747580","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T11:39:26Z","timestamp":1762774766000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747199.3747580"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,28]]},"references-count":40,"alternative-id":["10.1145\/3747199.3747580","10.1145\/3747199"],"URL":"https:\/\/doi.org\/10.1145\/3747199.3747580","relation":{},"subject":[],"published":{"date-parts":[[2025,7,28]]},"assertion":[{"value":"2025-11-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}