{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:58:06Z","timestamp":1725533886938},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642027765"},{"type":"electronic","value":"9783642027772"}],"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-02777-2_20","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T06:58:18Z","timestamp":1245999498000},"page":"195-208","source":"Crossref","is-referenced-by-count":4,"title":["Efficient Term-ITE Conversion for Satisfiability Modulo Theories"],"prefix":"10.1007","author":[{"given":"Hyondeuk","family":"Kim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"HoonSang","family":"Jin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","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":"20_CR2","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: Proceedings of the 27th Design Automation Conference, Orlando, FL, June 1990, pp. 40\u201345 (1990)","DOI":"10.1145\/123186.123222"},{"key":"20_CR3","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)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-31980-1_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2005","unstructured":"Jin, H., Han, H., Somenzi, F.: Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 287\u2013300. Springer, Heidelberg (2005)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: Prime clauses for fast enumeration of satisfying assignments to Boolean circuits. In: Proceedings of the Design Automation Conference, Anaheim, CA, June 2005, pp. 750\u2013753 (2005)","DOI":"10.1145\/1065579.1065775"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Jones, R.B., Dill, D.L., Burch, J.R.: Efficient validity checking for processor verification. In: Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, November 1995, pp. 2\u20136 (1995)","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"20_CR8","unstructured":"Karplus, K.: Representing Boolean functions with if-then-else DAGs. In Technical Report UCSC-CRL-88-28, Board of Studies in Computer Engineering, University of California at Santa Cruz, Santa Cruz, CA 95064 (December 1988)"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-540-70545-1_46","volume-title":"Computer Aided Verification","author":"H. Kim","year":"2008","unstructured":"Kim, H., Jin, H., Ravi, K., Spacek, P., Pierce, J., Kurshan, B., Somenzi, F.: Application of formal word-level analysis to constrained random simulation. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 487\u2013490. Springer, Heidelberg (2008)"},{"key":"20_CR10","doi-asserted-by":"crossref","first-page":"47","DOI":"10.3233\/SAT190029","volume":"3","author":"H. Kim","year":"2007","unstructured":"Kim, H., Jin, H., Somenzi, F.: Disequality management in integer difference logic via finite instantiations. Journal on Satisfiability, Boolean Modeling and Computation\u00a03, 47\u201366 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"issue":"2","key":"20_CR11","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"2008","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (2008)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/11817963_42","volume-title":"Computer Aided Verification","author":"K. Roe","year":"2006","unstructured":"Roe, K.: The heuristic theorem prover: Yet another SMT modulo theorem prover. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 467\u2013470. Springer, Heidelberg (2006)"},{"key":"20_CR14","unstructured":"http:\/\/smtcomp.org\/"},{"key":"20_CR15","unstructured":"http:\/\/vlsi.colorado.edu\/~vis"},{"key":"20_CR16","unstructured":"http:\/\/yices.csl.sri.com"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11814948_17","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Y. Yu","year":"2006","unstructured":"Yu, Y., Malik, S.: Lemma learning in SMT on linear constraints. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 142\u2013155. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02777-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T01:25:48Z","timestamp":1589937948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02777-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642027765","9783642027772"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02777-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}