{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T02:42:52Z","timestamp":1765593772001,"version":"3.48.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2024,7,4]],"date-time":"2024-07-04T00:00:00Z","timestamp":1720051200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,7,4]],"date-time":"2024-07-04T00:00:00Z","timestamp":1720051200000},"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":["J Syst Sci Complex"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s11424-024-3425-4","type":"journal-article","created":{"date-parts":[[2024,7,4]],"date-time":"2024-07-04T03:01:54Z","timestamp":1720062114000},"page":"2678-2700","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Sampling-Based Method to Estimate the Volume of Solution Space for Linear Arithmetic Constraints"],"prefix":"10.1007","volume":"38","author":[{"given":"Yan-Feng","family":"Xie","sequence":"first","affiliation":[]},{"given":"Chun-Ming","family":"Yuan","sequence":"additional","affiliation":[]},{"given":"Rui-Juan","family":"Jing","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,4]]},"reference":[{"key":"3425_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-031-37703-7_5","volume":"13965","author":"H Li","year":"2023","unstructured":"Li H, Xia B, and Zhao T, Local search for solving satisfiability of polynomial formulas, Lecture Notes in Computer Science, 2023, 13965): 87\u2013109.","journal-title":"Lecture Notes in Computer Science"},{"key":"3425_CR2","doi-asserted-by":"publisher","unstructured":"Hu X, Xu S, Tu Y, et al., CNF characterization of sets over \u2124n2 and its applications in cryptography, Journal of Systems Science & Complexity, 2023, DOI: https:\/\/doi.org\/10.1007\/s11424-024-3168-2.","DOI":"10.1007\/s11424-024-3168-2"},{"key":"3425_CR3","first-page":"825","volume":"185","author":"C Barrett","year":"2009","unstructured":"Barrett C, Sebastiani R, Seshia S A, et al., Satisfiability modulo theories, Handb. Satisfiability, 2009, 185): 825\u2013885.","journal-title":"Handb. Satisfiability"},{"key":"3425_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jsc.2019.07.017","volume":"100","author":"J H Davenport","year":"2020","unstructured":"Davenport J H, England M, Griggio A, et al., Symbolic computation and satisfiability checking, Journal of Symbolic Computation, 2020, 100): 1\u201310.","journal-title":"Journal of Symbolic Computation"},{"key":"3425_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer-Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett C, Conway C L, Deters M, et al., CVC4, Eds. by Gopalakrishnan G, Qadeer S, Computer-Aided Verification, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2011, 6806, DOI: https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14."},{"key":"3425_CR6","first-page":"337","volume":"4963","author":"L D Moura","year":"2008","unstructured":"Moura L D and Bjrner N, Z3: An efficient SMT solver, TACAS 2008, 2008, 4963: 337\u2013340.","journal-title":"TACAS 2008"},{"key":"3425_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification, Lecture Notes in Computer Science","author":"B Dutertre","year":"2014","unstructured":"Dutertre B, Yices 2.2, Eds. by Biere A, Bloem R, Computer Aided Verification, Lecture Notes in Computer Science, Springer, Cham, 2014, 8559, DOI: https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49."},{"key":"3425_CR8","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1007\/s10009-019-00549-9","volume":"22","author":"Y Li","year":"2020","unstructured":"Li Y, Wu W, and Feng Y, On ranking functions for single-path linear-constraint loops, International Journal on Software Tools Technology Transfer, 2020, 22): 655\u2013666.","journal-title":"International Journal on Software Tools Technology Transfer"},{"issue":"3","key":"3425_CR9","doi-asserted-by":"publisher","first-page":"1154","DOI":"10.1007\/s11424-022-1121-9","volume":"35","author":"W Lin","year":"2022","unstructured":"Lin W, Yang Z F, and Ding Z H, Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares programming, Journal of Systems Science & Complexity, 2022, 35(3): 1154\u20131172.","journal-title":"Journal of Systems Science & Complexity"},{"key":"3425_CR10","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A, Theory of Linear and Integer Programming, John Wiley & Sons, Inc., New York, 1986."},{"issue":"2","key":"3425_CR11","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s10957-008-9384-4","volume":"138","author":"C N Jones","year":"2008","unstructured":"Jones C N, Kerrigan E C, and Maciejowski J M, On polyhedral projection and parametric programming, Journal of Optimization Theory and Applications, 2008, 138(2): 207\u2013220.","journal-title":"Journal of Optimization Theory and Applications"},{"key":"3425_CR12","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/j.jsc.2019.07.021","volume":"100","author":"M Bromberger","year":"2019","unstructured":"Bromberger M, Sturm T, and Weidenbach C, A complete and terminating approach to linear integer solving, Journal of Symbolic Computation, 2019, 100): 102\u2013136.","journal-title":"Journal of Symbolic Computation"},{"key":"3425_CR13","first-page":"7","volume-title":"i>Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques (PACT\u2019 04)","author":"C Bastoul","year":"2004","unstructured":"Bastoul C, Code generation in the polyhedral model is easier than you think, Proceedings of the 13th International Conference on Parallel Architectures and Compilation Techniques (PACT\u2019 04), IEEE Computer Society, USA, 2004, 7\u201316."},{"key":"3425_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-642-11970-5_16","volume-title":"Compiler Construction","author":"M W Benabderrahmane","year":"2010","unstructured":"Benabderrahmane M W, Pouchet L N, Cohen A, et al., The polyhedral model is more widely applicable than you think, Compiler Construction, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 2010, 6011: 283\u2013303."},{"key":"3425_CR15","doi-asserted-by":"crossref","unstructured":"Zhao J and Di P, Optimizing the memory hierarchy by compositing automatic transformations on computations and data, 2020 53rd Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO), 2020, 427\u2013441.","DOI":"10.1109\/MICRO50266.2020.00044"},{"key":"3425_CR16","doi-asserted-by":"crossref","unstructured":"Liu S and Zhang J, Program analysis: From qualitative analysis to quantitative analysis (nier track), Proceedings of the 33rd International Conference on Software Engineering, IEEE Computer Society, 2011, 956\u2013959.","DOI":"10.1145\/1985793.1985957"},{"issue":"7","key":"3425_CR17","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J C King","year":"1976","unstructured":"King J C, Symbolic execution and program testing, Commun. ACM, 1976, 19(7): 385\u2013394.","journal-title":"Commun. ACM"},{"issue":"4","key":"3425_CR18","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","volume":"11","author":"C S P\u01ces\u01cereanu","year":"2009","unstructured":"P\u01ces\u01cereanu C S and Visser W, A survey of new trends in symbolic execution for software testing and analysis, Softw. Tools Technol. Transfer, 2009, 11(4): 339\u2013353.","journal-title":"Softw. Tools Technol. Transfer"},{"issue":"5","key":"3425_CR19","doi-asserted-by":"publisher","first-page":"967","DOI":"10.1137\/0217060","volume":"17","author":"M E Dyer","year":"1988","unstructured":"Dyer M E and Frieze A M, On the complexity of computing the volume of a polyhedron, SIAM J. Comput., 1988, 17(5): 967\u2013974.","journal-title":"SIAM J. Comput."},{"key":"3425_CR20","first-page":"216","volume":"3","author":"L G Khachiyan","year":"1988","unstructured":"Khachiyan L G, On the complexity of computing the volume of a polytope, Izv. Akad. Nauk SSSR, Eng. Cybern., 1988, 3): 216\u2013217.","journal-title":"Izv. Akad. Nauk SSSR, Eng. Cybern."},{"issue":"3","key":"3425_CR21","first-page":"199","volume":"44","author":"L G Khachiyan","year":"1989","unstructured":"Khachiyan L G, The problem of computing the volume of polytopes is NP-hard, Uspekhi Mat. Nauk, 1989, 44(3): 199\u2013200.","journal-title":"Uspekhi Mat. Nauk"},{"key":"3425_CR22","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.tcs.2016.10.019","volume":"743","author":"C Ge","year":"2018","unstructured":"Ge C, Ma F, Zhang P, et al., Computing and estimating the volume of the solution space of SMT (LA) constraints, Theoretical Computer Science, 2018, 743): 110\u2013129.","journal-title":"Theoretical Computer Science"},{"key":"3425_CR23","doi-asserted-by":"crossref","unstructured":"Emiris I Z and Fisikopoulos V, Efficient random-walk methods for approximating polytope volume, Proceedings of the 30th Annual Symposium on Computational Geometry, 2014, 318\u2013327.","DOI":"10.1145\/2582112.2582133"},{"issue":"2","key":"3425_CR24","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/s00224-014-9553-9","volume":"56","author":"M Zhou","year":"2015","unstructured":"Zhou M, He F, Song X, et al., Estimating the volume of solution space for satisfiability modulo linear real arithmetic, Theory of Computing Systems, 2015, 56(2): 347\u2013371.","journal-title":"Theory of Computing Systems"},{"key":"3425_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71458-5","volume-title":"Spherical Sampling","author":"W Freeden","year":"2018","unstructured":"Freeden W, Nashed M Z, and Schreiner M, Spherical Sampling, Birkh\u00e4user, Cham, 2018."},{"issue":"4","key":"3425_CR26","doi-asserted-by":"publisher","first-page":"1609","DOI":"10.1007\/s11424-023-1179-z","volume":"36","author":"Y Yao","year":"2023","unstructured":"Yao Y, Zou J, and Wang H, Optimal poisson subsampling for softmax regression, Journal of Systems Science & Complexity, 2023, 36(4): 1609\u20131625.","journal-title":"Journal of Systems Science & Complexity"},{"issue":"2","key":"3425_CR27","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1214\/aoms\/1177692644","volume":"43","author":"G Marsaglia","year":"1972","unstructured":"Marsaglia G, Choosing a point from the surface of a sphere, The Annals of Mathematical Statistics, 1972, 43(2): 645\u2013646.","journal-title":"The Annals of Mathematical Statistics"},{"issue":"8","key":"3425_CR28","first-page":"267","volume":"82","author":"M Gr\u00f6tschel","year":"1993","unstructured":"Gr\u00f6tschel M, Lovasz L, and Schrijver A, Geometric algorithms and combinatorial optimization, Advances in Mathematics, 1993, 82(8): 267\u2013267.","journal-title":"Advances in Mathematics"},{"key":"3425_CR29","doi-asserted-by":"crossref","unstructured":"Bruns W, Ichim B, and S\u00f8ger C, Normaliz: Algorithms for rational cones and affine monoids, 2010, http:\/\/www.math.uos.de\/normaliz.","DOI":"10.1016\/j.jalgebra.2010.01.031"}],"container-title":["Journal of Systems Science and Complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-024-3425-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11424-024-3425-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-024-3425-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T02:39:11Z","timestamp":1765593551000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11424-024-3425-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,4]]},"references-count":29,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["3425"],"URL":"https:\/\/doi.org\/10.1007\/s11424-024-3425-4","relation":{},"ISSN":["1009-6124","1559-7067"],"issn-type":[{"type":"print","value":"1009-6124"},{"type":"electronic","value":"1559-7067"}],"subject":[],"published":{"date-parts":[[2024,7,4]]},"assertion":[{"value":"13 November 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 April 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare no conflict of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of Interest"}}]}}