{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T14:41:54Z","timestamp":1761662514976},"publisher-location":"Berlin, Heidelberg","reference-count":16,"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_26","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T12:25:22Z","timestamp":1183033522000},"page":"272-286","source":"Crossref","is-referenced-by-count":45,"title":["Applying Logic Synthesis for Speeding Up SAT"],"prefix":"10.1007","author":[{"given":"Niklas","family":"Een","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Niklas","family":"S\u00f6rensson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Biere, A.: AIGER (AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs), http:\/\/fmv.jku.at\/aiger\/"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Boralv, A.: DAG-Aware Circuit Compression For Formal Verification. In: Proc.\u00a0ICCAD\u201904 (2004)","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Chen, D., Cong, J.: DAOmap: A Depth-Optimal Area Optimization Mapping Algorithm for FPGA Designs. In: ICCAD, pp. 752\u2013759 (2004)","DOI":"10.1109\/ICCAD.2004.1382677"},{"key":"26_CR4","unstructured":"Drechsler, R.: Using Synthesis Techniques in SAT Solvers. Technical Report, Intitute of Computer Schience, University of Bremen, Bremen, Germany (2004)"},{"key":"26_CR5","unstructured":"Een, N.: http:\/\/www.cs.chalmers.se\/~een\/SAT-2007"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","first-page":"61","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A., E\u00e9n, N.: 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":"26_CR7","doi-asserted-by":"crossref","unstructured":"Een, N., S\u00f6rensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modelling and Computation (JSAT)\u00a02 (2006)","DOI":"10.3233\/SAT190014"},{"key":"26_CR8","unstructured":"B.L.S. Group : ABC: A System for Sequential Synthesis and Verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b138245","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, Springer, Heidelberg (2005)"},{"key":"26_CR10","unstructured":"Minato, S.: Fast Generation of Irredundant Sum-Of-Products Forms from Binary Decision Diagrams. In: Proc.\u00a0SASIMI\u201992 (1992)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Proc.\u00a0DAC\u201906, pp. 532\u2013536 (2006)","DOI":"10.1145\/1146909.1147048"},{"issue":"2","key":"26_CR12","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1109\/TCAD.2006.887925","volume":"26","author":"A. Mishchenko","year":"2007","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.: Improvements to Technology Mapping for LUT-based FPGAs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a026(2), 240\u2013253 (2007)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"26_CR13","unstructured":"Sinz, C.: SAT-Race 2006 Benchmark Set (2006), http:\/\/fmv.jku.at\/sat-race-2006\/"},{"key":"26_CR14","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constr.\u00a0Math.\u00a0and Math.\u00a0Logic (1968)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors. In: Proc.\u00a0of Conf.\u00a0on Asia South Pacific Design Aut.\u00a0(ASP-DAC) (2004)","DOI":"10.1109\/ASPDAC.2004.1337587"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Zarpas","year":"2005","unstructured":"Zarpas, E.: Benchmarking SAT Solvers for Bounded Model Checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, Springer, Heidelberg (2005)"}],"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_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:05:08Z","timestamp":1605762308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72788-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727873","9783540727880"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72788-0_26","relation":{},"subject":[]}}