{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:14:32Z","timestamp":1759637672252},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_33","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T05:02:22Z","timestamp":1248498142000},"page":"453-468","source":"Crossref","is-referenced-by-count":13,"title":["Volume Computation for Boolean Combination of Linear Arithmetic Constraints"],"prefix":"10.1007","author":[{"given":"Feifei","family":"Ma","sequence":"first","affiliation":[]},{"given":"Sheng","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"7","key":"33_CR1","doi-asserted-by":"publisher","first-page":"830","DOI":"10.1109\/TC.2006.97","volume":"55","author":"S. Andrei","year":"2006","unstructured":"Andrei, S., Chin, W., Cheng, A.M.K., Lupu, M.: Automatic debugging of real-time systems based on incremental satisfiability counting. IEEE Trans. Computers\u00a055(7), 830\u2013842 (2006)","journal-title":"IEEE Trans. Computers"},{"key":"33_CR2","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Dalmao, S., Pitassi, T.: Algorithms and complexity results for #SAT and Bayesian inference. In: Proceedings of the 44th Symposium on Foundations of Computer Science (FOCS 2003), pp. 340\u2013351 (2003)","DOI":"10.1109\/SFCS.2003.1238208"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007), http:\/\/www.cs.nyu.edu\/acsys\/cvc3"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Behle, M., Eisenbrand, F.: 0\/1 vertex and facet enumeration with BDDs. In: Proceedings of the Workshop on Algorithm Engineering and Experiments (ALENEX 2007) (2007), http:\/\/www.mpi-inf.mpg.de\/~behle\/azove.html","DOI":"10.1137\/1.9781611972870.15"},{"key":"33_CR5","unstructured":"Berkelaar, M., Eikland, K., Notebaert, P.: The lp_solve Page, http:\/\/lpsolve.sourceforge.net\/"},{"key":"33_CR6","unstructured":"B\u00fceler, B., Enge, A., Fukuda, K.: Exact volume computation for polytopes: a practical study. Polytopes\u2013combinatorics and computation (1998), http:\/\/www.lix.polytechnique.fr\/Labo\/Andreas.Enge\/Vinci.html"},{"key":"33_CR7","doi-asserted-by":"crossref","unstructured":"Buse, R.P.L., Weimer, W.R.: The road not taken: Estimating path execution frequency statically. In: Proceedings of the 31st International Conference on Software Engineering (ICSE 2009) (2009)","DOI":"10.1109\/ICSE.2009.5070516"},{"key":"33_CR8","unstructured":"Davies, J., Bacchus, F.: Using more reasoning to improve #SAT solving. In: Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI 2007), pp. 185\u2013190 (2007)"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006), http:\/\/yices.csl.sri.com\/"},{"issue":"5","key":"33_CR10","doi-asserted-by":"publisher","first-page":"967","DOI":"10.1137\/0217060","volume":"17","author":"M. Dyer","year":"1988","unstructured":"Dyer, M., Frieze, A.: On the complexity of computing the volume of a polyhedron. SIAM J. Comput.\u00a017(5), 967\u2013974 (1988)","journal-title":"SIAM J. Comput."},{"key":"33_CR11","unstructured":"E\u00e9n, N., Sorensson, N.: The MiniSat Page, http:\/\/www.cs.chalmers.se\/Cs\/Research\/FormalMethods\/MiniSat\/"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"33_CR13","unstructured":"Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: From sampling to model counting. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 2293\u20132299 (2007)"},{"key":"33_CR14","unstructured":"Bayardo Jr., R.J., Pehoushek, J.D.: Counting models using connected components. In: Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on on Innovative Applications of Artificial Intelligence (AAAI\/IAAI 2000), pp. 157\u2013162 (2000)"},{"key":"33_CR15","volume-title":"The C Programming Language","author":"B.W. Kernighan","year":"1978","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C Programming Language. Prentice-Hall, Englewood Cliffs (1978)"},{"key":"33_CR16","volume-title":"Decision Procedures \u2014 An Algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures \u2014 An Algorithmic Point of View. Springer, Heidelberg (2008)"},{"issue":"4","key":"33_CR17","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"J.A.D. Loera","year":"2004","unstructured":"Loera, J.A.D., Hemmeckeb, R., Tauzera, J., Yoshidab, R.: Effective lattice point counting in rational convex polytopes. Journal of Symbolic Computation\u00a038(4), 1273\u20131302 (2004), http:\/\/www.math.ucdavis.edu\/~latte\/","journal-title":"Journal of Symbolic Computation"},{"key":"33_CR18","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. Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008), http:\/\/research.microsoft.com\/projects\/z3\/index.html"},{"issue":"6","key":"33_CR19","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"1-2","key":"33_CR20","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0004-3702(94)00092-1","volume":"82","author":"D. Roth","year":"1996","unstructured":"Roth, D.: On the hardness of approximate reasoning. Artif. Intell.\u00a082(1-2), 273\u2013302 (1996)","journal-title":"Artif. Intell."},{"key":"33_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-540-75560-9_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Samer","year":"2007","unstructured":"Samer, M., Szeider, S.: Algorithms for propositional model counting. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol.\u00a04790, pp. 484\u2013498. Springer, Heidelberg (2007)"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11499107_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"T. Sang","year":"2005","unstructured":"Sang, T., Beame, P., Kautz, H.A.: Heuristics for fast exact model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 226\u2013240. Springer, Heidelberg (2005)"},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/11499107_24","volume-title":"Theory and Applications of Satisfiability Testing","author":"W. Wei","year":"2005","unstructured":"Wei, W., Selman, B.: A new approach to model counting. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 324\u2013339. Springer, Heidelberg (2005)"},{"key":"33_CR24","doi-asserted-by":"crossref","unstructured":"Zhang, J.: Specification analysis and test data generation by solving boolean combinations of numeric constraints. In: Proceedings of the 1st Asia-Pacific Conference on Quality Software (APAQS 2000), pp. 267\u2013274 (2000)","DOI":"10.1109\/APAQ.2000.883800"},{"key":"33_CR25","unstructured":"Zhang, J.: Quantitative analysis of symbolic execution. Presented at the 28th International Computer Software and Applications Conference (COMPSAC 2004) (2004)"},{"issue":"2","key":"33_CR26","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1142\/S0218194001000487","volume":"11","author":"J. Zhang","year":"2001","unstructured":"Zhang, J., Wang, X.: A constraint solver and its application to path feasibility analysis. International Journal of Software Engineering and Knowledge Engineering\u00a011(2), 139\u2013156 (2001)","journal-title":"International Journal of Software Engineering and Knowledge Engineering"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T17:52:09Z","timestamp":1558461129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}