{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:46:21Z","timestamp":1746290781719},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727873"},{"type":"electronic","value":"9783540727880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72788-0_3","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T12:25:22Z","timestamp":1183033522000},"page":"4-9","source":"Crossref","is-referenced-by-count":15,"title":["Efficient Circuit to CNF Conversion"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daron","family":"Vroon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Brummayer, R., Biere, A.: Local two-level and-inverter graph minimization without blowup. In: Proc. 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS \u201906) (October 2006)"},{"key":"3_CR2","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.M.: 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":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"3_CR4","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSat - a SAT solver with conflict-clause minimization. In: Bacchus, F., Walsh, T. (eds.) Posters of the 8th international Conference on Theory and Applications of Satisfiability Testing (2005)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/11527695_15","volume-title":"Theory and Applications of Satisfiability Testing","author":"P. Jackson","year":"2005","unstructured":"Jackson, P., Sheridan, D.: Clause form conversions for Boolean circuits. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 183\u2013198. Springer, Heidelberg (2005)"},{"key":"3_CR6","volume-title":"ICCAD 2006, ACM-IEEE International Conference on Computer Aided Design","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: Automatic memory reductions for RTL-level verification. In: ICCAD 2006, ACM-IEEE International Conference on Computer Aided Design, ACM Press, New York (2006)"},{"key":"3_CR7","unstructured":"Manolios, P., Srinivasan, S.K., Vroon, D.: BAT: The Bit-level Analysis Tool (2006), Available from http:\/\/www.cc.gatech.edu\/~manolios\/bat\/"},{"key":"3_CR8","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)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115\u2013125. Consultants Bureau, New York-London (1962)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"3_CR10","first-page":"310","volume-title":"ASP-DAC \u201904: Proceedings of the 2004 conference on Asia South Pacific design automation","author":"M.N. Velev","year":"2004","unstructured":"Velev, M.N.: Efficient translation of boolean formulas to cnf in formal verification of microprocessors. In: ASP-DAC \u201904: Proceedings of the 2004 conference on Asia South Pacific design automation, pp. 310\u2013315. IEEE Computer Society Press, Los Alamitos (2004)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72788-0_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:05:10Z","timestamp":1605762310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72788-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727873","9783540727880"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72788-0_3","relation":{},"subject":[]}}