{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:17:02Z","timestamp":1725560222906},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_23","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"315-321","source":"Crossref","is-referenced-by-count":30,"title":["The MathSAT 3 System"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[]},{"given":"Peter","family":"van Rossum","sequence":"additional","affiliation":[]},{"given":"Stephan","family":"Schulz","sequence":"additional","affiliation":[]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Pub. Co, Amsterdam (1954)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11527695_2","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Armando","year":"2005","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"23_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 195\u2013210. Springer, Heidelberg (2002)"},{"key":"23_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-45470-5_22","volume-title":"Artificial Intelligence, Automated Reasoning, and Symbolic Computation","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: Integrating boolean and mathematical solving: Foundations, basic algorithms, and requirements. In: Calmet, J., Benhamou, B., Caprotti, O., H\u00e9nocque, L., Sorge, V. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol.\u00a02385, pp. 231\u2013245. Springer, Heidelberg (2002)"},{"issue":"4","key":"23_CR5","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1145\/504704.504705","volume":"8","author":"G.J. Badros","year":"2001","unstructured":"Badros, G.J., Borning, A., Stuckey, P.J.: The Cassowary Linear Arithmetic Constraint Solving Algorithm. ACM Trans. on Computer-Human Interaction\u00a08(4), 267\u2013306 (2001)","journal-title":"ACM Trans. on Computer-Human Interaction"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/11513988_34","volume-title":"Computer Aided Verification","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient satisfiability modulo theories via delayed theory combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 335\u2013349. Springer, Heidelberg (2005)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"23_CR8","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: MathSAT: Tight Integration of SAT and Mathematical Decision Procedure. Journal of Automated Reasoning (to appear)"},{"issue":"2","key":"23_CR9","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B.V. Cherkassky","year":"1999","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-Cycle Detection Algorithms. Mathematical Programming\u00a085(2), 277\u2013311 (1999)","journal-title":"Mathematical Programming"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"23_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":"23_CR13","unstructured":"Gomes, C.P., Selman, B., Kautz, H.A.: Boosting Combinatorial Search Through Randomization. In: AAAI\/IAAI 1998, pp. 431\u2013437. AAAI Press \/ The MIT Press (1998)"},{"issue":"3","key":"23_CR14","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/129393.129398","volume":"14","author":"J. Jaffar","year":"1992","unstructured":"Jaffar, J., Michaylov, S., Stuckey, P.J., Yap, R.H.C.: The CLP(R) Language and System. ACM Trans. on Programming Languages and Systems\u00a014(3), 339\u2013395 (1992)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"5","key":"23_CR15","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. on Computers"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1145\/378239.379017","volume-title":"DAC 2001","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC 2001, pp. 530\u2013535. ACM, New York (2001)"},{"key":"23_CR17","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-39813-4_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence Closure with Integer Offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol.\u00a02850, pp. 78\u201390. Springer, Heidelberg (2003)"},{"key":"23_CR18","unstructured":"Omega, \n                  \n                    http:\/\/www.cs.umd.edu\/projects\/omega"},{"issue":"2\/3","key":"23_CR19","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"AI Communications"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,17]],"date-time":"2019-03-17T06:35:43Z","timestamp":1552804543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11532231_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}