{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:31:27Z","timestamp":1762101087371},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_37","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T08:51:59Z","timestamp":1286182319000},"page":"519-534","source":"Crossref","is-referenced-by-count":8,"title":["Improving Resource-Unaware SAT Solvers"],"prefix":"10.1007","author":[{"given":"Steffen","family":"H\u00f6lldobler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ari","family":"Saptawijaya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"37_CR1","unstructured":"HPCToolkit, http:\/\/hpctoolkit.org\/"},{"key":"37_CR2","unstructured":"ICCL SAT project group, http:\/\/www.wv.inf.tu-dresden.de\/Research\/SATSolving\/"},{"key":"37_CR3","unstructured":"PAPI library, http:\/\/icl.cs.utk.edu\/papi\/"},{"key":"37_CR4","unstructured":"Baldow, C., Gr\u00e4ter, F., H\u00f6lldobler, S., Manthey, N., Seelemann, M., Steinke, P., Wernhard, C., Winkler, K., Zenker, E.: HydraSAT 2009.3 solver description. SAT 2009 Competitive Event Booklet, http:\/\/www.cril.univ-artois.fr\/SAT09\/solvers\/booklet.pdf"},{"key":"37_CR5","unstructured":"B\u00e9jar, R., Many\u00e0, F.: Solving the round robin problem using propositional logic. In: Procs. 17th National Conf. on Artificial Intelligence and 12th Conf. on Innovative Applications of Artificial Intelligence (2000)"},{"key":"37_CR6","unstructured":"Bonwick, J.: The slab allocator: an object-caching kernel memory allocator. In: Proceedings of the USENIX Summer 1994 Technical Conference (1994)"},{"key":"37_CR7","first-page":"99","volume":"6","author":"G. Chu","year":"2009","unstructured":"Chu, G., Harwood, A., Stuckey, P.J.: Cache conscious data structures for boolean satisfiability solvers. JSAT\u00a06, 99\u2013120 (2009)","journal-title":"JSAT"},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Procs. 3rd Annual ACM Symposium on Theory of Computing (1971)","DOI":"10.1145\/800157.805047"},{"issue":"7","key":"37_CR9","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"37_CR11","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: MiniSAT - a SAT solver with conflict-clause minimization. In: Poster - 8th SAT (2005)"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, Springer, Heidelberg (2007)"},{"key":"37_CR13","volume-title":"Computer Architecture - A Quantitative Approach","author":"J. Hennessy","year":"1996","unstructured":"Hennessy, J., Patterson, D.: Computer Architecture - A Quantitative Approach. Morgan Kaufmann, San Francisco (1996)"},{"key":"37_CR14","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Procs. 10th European Conference on Artificial Intelligence (1992)"},{"key":"37_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"I. Lynce","year":"2006","unstructured":"Lynce, I., Marques-Silva, J.: SAT in bioinformatics: making the case with haplotype inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, Springer, Heidelberg (2006)"},{"key":"37_CR16","unstructured":"Manthey, N.: riss 2010 solver description. SAT Race (2010) (submitted to), http:\/\/www.ki.inf.tu-dresden.de\/~norbert\/webdata\/data\/riss-short.pdf"},{"key":"37_CR17","unstructured":"Manthey, N., Saptawijaya, A.: Towards improving the resource usage of SAT-solvers. In: Pragmatics of SAT Workshop (2010) (to appear)"},{"key":"37_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J.P. Marques-Silva","year":"1996","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A new search algorithm for satisfiability. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"37_CR20","unstructured":"Pipatsrisawat, K., Darwiche, A.: RSat solver description for SAT competition, SAT, Competitive Event Booklet (2009), http:\/\/www.cril.univ-artois.fr\/SAT09\/solvers\/booklet.pdf"},{"key":"37_CR21","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"37_CR22","unstructured":"Ryan, L.O.: Efficient algorithms for clause learning SAT solvers. Master\u2019s thesis, Simon Fraser University, Canada (2004)"},{"key":"37_CR23","unstructured":"S\u00f6rensson, N., E\u00e9n, N.: MiniSAT 2.1 and MiniSAT++ 1.0 - SAT race, editions. SAT, Competitive Event Booklet (2008), http:\/\/www.cril.univ-artois.fr\/SAT09\/solvers\/booklet.pdf"},{"key":"37_CR24","unstructured":"van Gelder, A.: Generalizations of watched literals for backtracking search. In: Seventh International Symposium on AI and Mathematics (2002)"},{"key":"37_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-24605-3_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"L. Zhang","year":"2004","unstructured":"Zhang, L., Malik, S.: Cache performance of SAT solvers: a case study for efficient implementation of algorithms. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 287\u2013298. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T02:02:26Z","timestamp":1559700146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}