{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T16:11:44Z","timestamp":1779379904618,"version":"3.53.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540208518","type":"print"},{"value":"9783540246053","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_37","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:50:35Z","timestamp":1280379035000},"page":"502-518","source":"Crossref","is-referenced-by-count":1077,"title":["An Extensible SAT-solver"],"prefix":"10.1007","author":[{"given":"Niklas","family":"E\u00e9n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Niklas","family":"S\u00f6rensson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Generic ILP vs. Specialized 0-1 ILP: an Update. In: International Conference on Computer Aided Design, ICCAD (2002)","DOI":"10.1145\/774572.774638"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic Model Checking using SAT procedures instead of BDDs. In: Proceedings of Design Automation Conference, DAC 1999 (1999)","DOI":"10.21236\/ADA360973"},{"key":"37_CR3","unstructured":"Claessen, K., S\u00f6rensson, N.: New Techniques that Improve MACEstyle Finite Model Finding. In: CADE-19, Workshop W4. Model Computation \u2013 Principles, Algorithms, Applications (2003)"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Davis, M., Logman, M., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05 (1962)","DOI":"10.1145\/368273.368557"},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal Induction by Incremental SAT Solving. In: Proc. of First International Workshop on Bounded Model Checking (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"Larrabee, T.: Test Pattern Generation Using Boolean Satisfiability. IEEE Transactions on Computer-Aided Design, vol\u00a011(1) (1992)","DOI":"10.1109\/43.108614"},{"key":"37_CR7","volume-title":"ICCAD","author":"J.P. Marques-Silva","year":"1996","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP \u2013 A New Search Algorithm for Satisfiability. In: ICCAD. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 38th Design Automation Conference (2001)","DOI":"10.1145\/378239.379017"},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient Conflict Driven Learning in Boolean Satisfiability Solver. In: Proc. of the International Conference on Computer Aided Design, ICCAD (2001)","DOI":"10.1145\/774572.774637"},{"key":"37_CR10","volume-title":"Proc. 38th Conf. on Design Automation","author":"J. Whittemore","year":"2001","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: SATIRE: A New Incremental Satisfiability Engine. In: Proc. 38th Conf. on Design Automation. ACM Press, New York (2001)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:54:13Z","timestamp":1559332453000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}