{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T04:04:30Z","timestamp":1750565070623,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_4","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"42-59","source":"Crossref","is-referenced-by-count":14,"title":["Satisfiability Modulo Theories and Assignments"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). doi: 10.1007\/11916277_35"},{"key":"4_CR2","unstructured":"Bonacina, M.P.: On conflict-driven reasoning. In: Dutertre, B., Shankar, N. (eds.) Proceedings of the Sixth Workshop on Automated Formal Methods (AFM), at the Ninth NASA Formal Methods Symposium (NFM), pp. 1\u20139 (2017, to appear). http:\/\/fm.csl.sri.com\/AFM17\/"},{"key":"4_CR3","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: A model-constructing framework for theory combination. Technical Report 99\/2016, Dipartimento di Informatica, Universit\u00e0 degli Studi di Verona, Verona, Italy, EU. https:\/\/hal.archives-ouvertes.fr\/hal-01425305 , also Technical report of SRI International and INRIA - CNRS - \u00c9cole Polytechnique; Revised April 2017"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15297-9_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Cotton","year":"2010","unstructured":"Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77\u201391. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15297-9_8"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura","year":"2013","unstructured":"Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35873-9_1"},{"key":"4_CR6","unstructured":"Ganzinger, H., Rue\u00df, H., Shankar, N.: Modularity and refinement in inference systems. Technical report CSL-SRI-04-02, Computer Science Laboratory, SRI International, Menlo Park, CA, USA (2004)"},{"key":"4_CR7","unstructured":"Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Cabodi, G., Singh, S. (eds.) Proceedings of the Twelfth International Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE (2012)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-52234-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Jovanovi\u0107","year":"2017","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330\u2013346. Springer, Heidelberg (2017). doi: 10.1007\/978-3-319-52234-0_18"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of the Thirteenth Conference on Formal Methods in Computer Aided Design (FMCAD). ACM and IEEE (2013)","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-22438-6_26","volume-title":"Automated Deduction \u2013 CADE-23","author":"D Jovanovi\u0107","year":"2011","unstructured":"Jovanovi\u0107, D., Moura, L.: Cutting to the chase: solving linear integer arithmetic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 338\u2013353. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_26"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_27"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-04244-7_41","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K Korovin","year":"2009","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509\u2013523. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04244-7_41"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCoS 2007. LNCS (LNAI), vol. 4720, pp. 1\u201327. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74621-8_1"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Marques Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131\u2013153. IOS Press (2009)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462\u2013476. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_35"},{"issue":"2","key":"4_CR16","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Prog. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/11591191_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Wang","year":"2005","unstructured":"Wang, C., Ivan\u010di\u0107, F., Ganai, M., Gupta, A.: Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 322\u2013336. Springer, Heidelberg (2005). doi: 10.1007\/11591191_23"},{"key":"4_CR18","unstructured":"Wolfman, S.A., Weld, D.S.: The LPSAT engine and its application to resource planning. In: Dean, T. (ed.) Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI), vol. 1, pp. 310\u2013316. Morgan Kaufmann Publishers (1999)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-319-40970-2_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"A Zelji\u0107","year":"2016","unstructured":"Zelji\u0107, A., Wintersteiger, C.M., R\u00fcmmer, P.: Deciding bit-vector formulas with mcSAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 249\u2013266. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-40970-2_16"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:18Z","timestamp":1750533858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}