{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:18:03Z","timestamp":1766135883682,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_15","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"215-230","source":"Crossref","is-referenced-by-count":47,"title":["Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. CUP (2003)"},{"issue":"4","key":"15_CR2","doi-asserted-by":"publisher","first-page":"710","DOI":"10.1137\/1018115","volume":"18","author":"E. Balas","year":"1976","unstructured":"Balas, E., Padberg, M.W.: Set partitioning: A survey. SIAM Review\u00a018(4), 710\u2013760 (1976)","journal-title":"SIAM Review"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"issue":"1","key":"15_CR4","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L. Berman","year":"1980","unstructured":"Berman, L.: The complexity of logical theories. Theoretical Computer Science\u00a011(1), 71\u201377 (1980)","journal-title":"Theoretical Computer Science"},{"key":"15_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C. Bouillaguet","year":"2007","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using first-order theorem provers in a data structure verification system. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, Springer, Heidelberg (2007)"},{"key":"15_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing","author":"D. Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing. Springer, Heidelberg (2001)"},{"issue":"5","key":"15_CR8","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1016\/j.orl.2005.09.008","volume":"34","author":"F. Eisenbrand","year":"2006","unstructured":"Eisenbrand, F., Shmonina, G.: Carath\u00e9odory bounds for integer cones. Operations Research Letters\u00a034(5), 564\u2013568 (2006), \n                    \n                      http:\/\/dx.doi.org\/10.1016\/j.orl.2005.09.008","journal-title":"Operations Research Letters"},{"key":"15_CR9","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S. Feferman","year":"1959","unstructured":"Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundamenta Mathematicae\u00a047, 57\u2013103 (1959)","journal-title":"Fundamenta Mathematicae"},{"issue":"3-4","key":"15_CR10","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S. Ghilardi","year":"2005","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning\u00a033(3-4), 221\u2013249 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR11","volume-title":"Theory of Computation","author":"D. Kozen","year":"2006","unstructured":"Kozen, D.: Theory of Computation. Springer, Heidelberg (2006)"},{"key":"15_CR12","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"key":"15_CR13","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning (2006), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/s10817-006-9042-1","DOI":"10.1007\/s10817-006-9042-1"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL 2005) (2005)","DOI":"10.1016\/j.entcs.2005.01.022"},{"key":"15_CR16","unstructured":"Lev, I.: Precise understanding of natural language. Stanford Univeristy PhD dissertation draft (February 2007)"},{"key":"15_CR17","unstructured":"Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (August 2005)"},{"key":"15_CR18","unstructured":"Marriott, K., Odersky, M.: Negative boolean constraints. Technical Report 94\/203, Monash University (August 1994)"},{"key":"15_CR19","volume-title":"Automated Deduction. A Basis for Applications","author":"H.J. Ohlbach","year":"1998","unstructured":"Ohlbach, H.J., Koehler, J.: How to extend a formal system with a boolean algebra component. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction. A Basis for Applications, vol.\u00a0III, Kluwer Academic Publishers, Dordrecht (1998)"},{"issue":"4","key":"15_CR20","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C.H. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM\u00a028(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"issue":"3","key":"15_CR21","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10849-005-5791-1","volume":"14","author":"I. Pratt-Hartmann","year":"2005","unstructured":"Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information\u00a014(3), 369\u2013395 (2005)","journal-title":"Journal of Logic, Language and Information"},{"key":"15_CR22","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: ESCoR: Empirically Successful Computerized Reasoning, vol. 192 (2006)"},{"key":"15_CR23","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa (2006), Available at \n                    \n                      http:\/\/www.SMT-LIB.org"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Databases and Information Systems","author":"P. Revesz","year":"2004","unstructured":"Revesz, P.: Quantifier-elimination for the first-order theory of boolean algebras with linear cardinality constraints. In: Bencz\u00far, A.A., Demetrovics, J., Gottlob, G. (eds.) ADBIS 2004. LNCS, vol.\u00a03255, Springer, Heidelberg (2004)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11547686_13","volume-title":"Advances in Databases and Information Systems","author":"P.Z. Revesz","year":"2005","unstructured":"Revesz, P.Z.: The expressivity of constraint query languages with boolean algebra linear cardinality constraints. In: Eder, J., Haav, H.-M., Kalja, A., Penjam, J. (eds.) ADBIS 2005. LNCS, vol.\u00a03631, pp. 167\u2013182. Springer, Heidelberg (2005)"},{"key":"15_CR26","unstructured":"Seb\u00f6, A.: Hilbert bases, Caratheodory\u2019s theorem and combinatorial optimization. In: Kannan, R., Pulleyblank, W. (eds.) Integer Programming and Combinatorial Optimization I, University of Waterloo Press (1990)"},{"issue":"5","key":"15_CR27","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1137\/0220053","volume":"20","author":"S. Toda","year":"1991","unstructured":"Toda, S.: PP is as hard as the polynomial-time hierarchy. SIAM Journal on Computing\u00a020(5), 865\u2013877 (1991)","journal-title":"SIAM Journal on Computing"},{"key":"15_CR28","doi-asserted-by":"publisher","first-page":"509","DOI":"10.2307\/2371182","volume":"57","author":"H. Whitney","year":"1935","unstructured":"Whitney, H.: On the abstract properties of linear independence. American Journal of Mathematics\u00a057, 509\u2013533 (1935)","journal-title":"American Journal of Mathematics"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Zarba, C.G.: Combining sets with cardinals. J. of Automated Reasoning 34(1) (2005)","DOI":"10.1007\/s10817-005-3075-8"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:01Z","timestamp":1619517181000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}