{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T02:53:14Z","timestamp":1725677594065},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642296994"},{"type":"electronic","value":"9783642297007"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29700-7_23","type":"book-chapter","created":{"date-parts":[[2012,4,28]],"date-time":"2012-04-28T12:25:56Z","timestamp":1335615956000},"page":"247-258","source":"Crossref","is-referenced-by-count":4,"title":["Solving Generalized Optimization Problems Subject to SMT Constraints"],"prefix":"10.1007","author":[{"given":"Feifei","family":"Ma","sequence":"first","affiliation":[]},{"given":"Jun","family":"Yan","sequence":"additional","affiliation":[]},{"given":"Jian","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","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.W. Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007), \n                  \n                    http:\/\/www.cs.nyu.edu\/acsys\/cvc3"},{"key":"23_CR2","unstructured":"Cheng, K.C., Yap, R.H.C.: Search space reduction and Russian doll search. In: Proceedings of the 22nd AAAI Conference on Artificial Intelligence (AAAI 2007) (2007)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability Modulo the Theory of Costs: Foundations and Applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 99\u2013113. Springer, Heidelberg (2010)"},{"key":"23_CR4","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., de Moura, L.: 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), \n                  \n                    http:\/\/yices.csl.sri.com\/"},{"key":"23_CR5","unstructured":"E\u00e9n, N., Sorensson, N.: The MiniSat Page (2011), \n                  \n                    http:\/\/minisat.se\/"},{"key":"23_CR6","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":"23_CR7","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1287\/ijoc.14.4.295.2828","volume":"14","author":"J.N. Hooker","year":"2002","unstructured":"Hooker, J.N.: Logic, optimization, and constraint programming. INFORMS Journal on Computing\u00a014, 295\u2013321 (2002)","journal-title":"INFORMS Journal on Computing"},{"key":"23_CR8","unstructured":"IBM. Cplex, \n                  \n                    http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimization-studio\/"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Hooker, J.N., Osorio, M.A.: Mixed logical-linear programming. Discrete Appl. Math.\u00a096-97, 395\u2013442 (October 1999)","DOI":"10.1016\/S0166-218X(99)00100-6"},{"key":"23_CR10","unstructured":"Kroening, D., Strichman, O.: Decision Procedures. Springer (2008)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-02959-2_33","volume-title":"Automated Deduction \u2013 CADE-22","author":"F. Ma","year":"2009","unstructured":"Ma, F., Liu, S., Zhang, J.: Volume Computation for Boolean Combination of Linear Arithmetic Constraints. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 453\u2013468. Springer, Heidelberg (2009)"},{"key":"23_CR12","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 de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008), \n                  \n                    http:\/\/research.microsoft.com\/projects\/z3\/index.html"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 156\u2013169. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Frontiers in Algorithmics and Algorithmic Aspects in Information and Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29700-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T00:34:33Z","timestamp":1558312473000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29700-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642296994","9783642297007"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29700-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}