{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T04:03:48Z","timestamp":1760241828735,"version":"build-2065373602"},"reference-count":26,"publisher":"MDPI AG","issue":"9","license":[{"start":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T00:00:00Z","timestamp":1537228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61103136"],"award-info":[{"award-number":["61103136"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>The satisfiability modulo theories (SMT) problem is to decide the satisfiability of a logical formula with respect to a given background theory. This work studies the counting version of SMT with respect to linear integer arithmetic (LIA), termed SMT(LIA). Specifically, the purpose of this paper is to count the number of solutions (volume) of a SMT(LIA) formula, which has many important applications and is computationally hard. To solve the counting problem, an approximate method that employs a recent Markov Chain Monte Carlo (MCMC) sampling strategy called \u201cflat histogram\u201d is proposed. Furthermore, two refinement strategies are proposed for the sampling process and result in two algorithms, MCMC-Flat1\/2 and MCMC-Flat1\/t, respectively. In MCMC-Flat1\/t, a pseudo sampling strategy is introduced to evaluate the flatness of histograms. Experimental results show that our MCMC-Flat1\/t method can achieve good accuracy on both structured and random instances, and our MCMC-Flat1\/2 is scalable for instances of convex bodies with up to 7 variables.<\/jats:p>","DOI":"10.3390\/a11090142","type":"journal-article","created":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T11:52:29Z","timestamp":1537271549000},"page":"142","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Estimating the Volume of the Solution Space of SMT(LIA) Constraints by a Flat Histogram Method"],"prefix":"10.3390","volume":"11","author":[{"given":"Wei","family":"Gao","sequence":"first","affiliation":[{"name":"School of Astronautics, Beihang University, Beijing 100191, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3628-0991","authenticated-orcid":false,"given":"Hengyi","family":"Lv","sequence":"additional","affiliation":[{"name":"Changchun Institute of Optics, Fine Mechanics and Physics, Chinese Academy of Sciences, Changchun 130033, China"}]},{"given":"Qiang","family":"Zhang","sequence":"additional","affiliation":[{"name":"Beijing Aerospace Control Center, Beijing 100094, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0653-3663","authenticated-orcid":false,"given":"Dunbo","family":"Cai","sequence":"additional","affiliation":[{"name":"Hubei Provincial Key Laboratory of Intelligent Robot, Wuhan Institute of Technology, Wuhan 430205, China"}]}],"member":"1968","published-online":{"date-parts":[[2018,9,18]]},"reference":[{"key":"ref_1","first-page":"825","article-title":"Satisfiability modulo theories","volume":"Volume 185","author":"Biere","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Dyer, M.E., Frieze, A.M., and Kannan, R. (1989, January 14\u201317). A random polynomial time algorithm for approximating the volume of convex bodies. Proceedings of the 21st Annual ACM Symposium on Theory of Computing, Seattle, WA, USA.","DOI":"10.1145\/73007.73043"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"967","DOI":"10.1137\/0217060","article-title":"On the complexity of computing the volume of a polyhedron","volume":"17","author":"Dyer","year":"1988","journal-title":"SIAM J. Comput."},{"key":"ref_4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","article-title":"A compositional modelling and analysis framework for stochastic hybrid systems","volume":"43","author":"Hahn","year":"2013","journal-title":"Form. Methods Syst. Des."},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Immler, F. (2015, January 11\u201318). Verified reachability analysis of continuous systems\u2019. Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems\u201421st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK.","DOI":"10.1007\/978-3-662-46681-0_3"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Hadarean, L., Barrett, C., Reynolds, A., Tinelli, C., and Deters, M. (2015, January 24\u201328). Fine grained SMT proofs for the theory of fixed-width bit-vectors. Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-20, Suva, Fiji.","DOI":"10.1007\/978-3-662-48899-7_24"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"1978","DOI":"10.1016\/j.jss.2013.02.061","article-title":"An orchestrated survey of methodologies for automated software test case generation","volume":"86","author":"Anand","year":"2013","journal-title":"J. Syst. Softw."},{"key":"ref_8","unstructured":"Zhang, J. (2000, January 30\u201331). Specification analysis and test data generation by solving Boolean combinations of numeric constraints. Proceedings of the First Asia-Pacific Conference on Quality Software, Hongkong, China."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.tcs.2016.10.019","article-title":"Computing and estimating the volume of the solution space of SMT (LA) constraints","volume":"743","author":"Ge","year":"2018","journal-title":"Theor. Comput. Sci."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.ipl.2008.01.007","article-title":"An efficient method to generate feasible paths for basis path testing","volume":"107","author":"Yan","year":"2008","journal-title":"Inform. Process. Lett."},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1142\/S0218194001000487","article-title":"A constraint solver and its application to path feasibility analysis","volume":"11","author":"Zhang","year":"2001","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"1477","DOI":"10.1109\/43.664229","article-title":"Performance analysis of embedded software using implicit path enumeration","volume":"16","author":"Li","year":"1997","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1145\/989393.989451","article-title":"Improving data-flow analysis with path profiles","volume":"39","author":"Ammons","year":"2004","journal-title":"ACM Sigplan Not."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Wang, F., and Landau, D.P. (2001). Efficient, multiple-range random walk algorithm to calculate the density of states. Phys. Rev. Lett., 86.","DOI":"10.1103\/PhysRevLett.86.2050"},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Whitmer, J.K., Chiu, C.C., Joshi, A.A., and De Pablo, J.J. (2014). Basis function sampling: A new paradigm for material property computation. Phys. Rev. Lett., 113.","DOI":"10.1103\/PhysRevLett.113.190602"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Whitmer, J.K., Fluitt, A.M., Antony, L., Qin, J., McGovern, M., and De Pablo, J.J. (2015). Sculpting bespoke mountains: Determining free energies with basis expansions. J. Chem. Phys., 143.","DOI":"10.1063\/1.4927147"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Zablotskiy, S.V., Ivanov, V.A., and Paul, W. (2016). Multidimensional stochastic approximation Monte Carlo. Phys. Rev. E, 93.","DOI":"10.1103\/PhysRevE.93.063303"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Ma, F., Liu, S., and Zhang, J. (2009, January 2\u20137). Volume computation for boolean combination of linear arithmetic constraints. Proceedings of the Automated Deduction\u2014CADE-22, 22nd International Conference on Automated Deduction, Montreal, QC, Canada.","DOI":"10.1007\/978-3-642-02959-2_33"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Mistry, R., and Vardi, M.Y. (2016, January 12\u201317). Approximate Probabilistic Inference via Word-Level Counting. Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, Phoenix, AZ, USA.","DOI":"10.1609\/aaai.v30i1.10416"},{"key":"ref_20","unstructured":"Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., and Malik, S. (2016, January 12\u201313). Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. Proceedings of the AAAI\u201916 Workshop: Beyond NP, Phoenix, AZ, USA."},{"key":"ref_21","unstructured":"Chakraborty, S., Meel, K.S., and Vardi, M.Y. (2016, January 9\u201315). Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic SAT calls. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, New York, NY, USA."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Ermon, S., Gomes, C.P., and Selman, B. (2010, January 6\u201310). Computing the density of states of Boolean formulas. Proceedings of the Principles and Practice of Constraint Programming\u2014CP 2010\u201416th International Conference, Scotland, UK.","DOI":"10.1007\/978-3-642-15396-9_6"},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","article-title":"Effective lattice point counting in rational convex polytopes","volume":"38","author":"Hemmecke","year":"2004","journal-title":"J. Symb. Comput."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/s00224-014-9553-9","article-title":"Estimating the Volume of Solution Space for Satisfiability Modulo Linear Real Arithmetic","volume":"56","author":"Zhou","year":"2015","journal-title":"Theor. Comput. Syst."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Belardinelli, R.E., and Pereyra, V.D. (2007). Fast algorithm to calculate density of states. Phys. Rev. E, 75.","DOI":"10.1103\/PhysRevE.75.046701"},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1214\/12-AAP913","article-title":"The Wang-Landau algorithm reaches the flat histogram criterion in finite time","volume":"24","author":"Jacob","year":"2014","journal-title":"Ann. Appl. Probab."}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/11\/9\/142\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T15:21:12Z","timestamp":1760196072000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/11\/9\/142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,18]]},"references-count":26,"journal-issue":{"issue":"9","published-online":{"date-parts":[[2018,9]]}},"alternative-id":["a11090142"],"URL":"https:\/\/doi.org\/10.3390\/a11090142","relation":{},"ISSN":["1999-4893"],"issn-type":[{"type":"electronic","value":"1999-4893"}],"subject":[],"published":{"date-parts":[[2018,9,18]]}}}