{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T21:44:52Z","timestamp":1725745492351},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642409417"},{"type":"electronic","value":"9783642409424"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40942-4_6","type":"book-chapter","created":{"date-parts":[[2013,8,19]],"date-time":"2013-08-19T23:43:31Z","timestamp":1376955811000},"page":"61-73","source":"Crossref","is-referenced-by-count":4,"title":["Parallel Variable Elimination on CNF Formulas"],"prefix":"10.1007","author":[{"given":"Kilian","family":"Gebhardt","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Manthey","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Grasp \u2013 a new search algorithm for satisfiability. In: Proc. 1996 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1996, pp. 220\u2013227 (1996)"},{"key":"6_CR2","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1145\/309847.309942","volume-title":"Proc. 36th Annual ACM\/IEEE Design Automation Conference, DAC 1999","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Annual ACM\/IEEE Design Automation Conference, DAC 1999, pp. 317\u2013320. ACM, New York (1999)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: DAC 2002, pp. 731\u2013736 (2002)","DOI":"10.1109\/DAC.2002.1012719"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-31087-4_18","volume-title":"Advanced Research in Applied Artificial Intelligence","author":"P. Gro\u00dfmann","year":"2012","unstructured":"Gro\u00dfmann, P., H\u00f6lldobler, S., Manthey, N., Nachtigall, K., Opitz, J., Steinke, P.: Solving periodic event scheduling problems with SAT. In: Jiang, H., Ding, W., Ali, M., Wu, X. (eds.) IEA\/AIE 2012. LNCS, vol.\u00a07345, pp. 166\u2013175. Springer, Heidelberg (2012)"},{"key":"6_CR5","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. 38th Annual Design Automation Conference, DAC 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"6_CR6","unstructured":"Ryan, L.O.: Efficient algorithms for clause learning SAT solvers. Master\u2019s thesis, Simon Fraser University, Canada (2004)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-642-16242-8_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. H\u00f6lldobler","year":"2010","unstructured":"H\u00f6lldobler, S., Manthey, N., Saptawijaya, A.: Improving resource-unaware SAT solvers. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 519\u2013534. Springer, Heidelberg (2010)"},{"key":"6_CR8","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proc. 21st Int. Joint Conf. on Artifical Intelligence, IJCAI 2009, pp. 399\u2013404 (2009)"},{"key":"6_CR9","unstructured":"Huang, J.: The effect of restarts on the efficiency of clause learning. In: Proc. 20th International Joint Conference on Artifical Intelligence, IJCAI 2007, pp. 2318\u20132323 (2007)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-36742-7_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Belov","year":"2013","unstructured":"Belov, A., J\u00e4rvisalo, M., Marques-Silva, J.: Formula preprocessing in mus extraction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 108\u2013123. Springer, Heidelberg (2013)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-31612-8_20","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Preprocessing in incremental sat. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 256\u2013269. Springer, Heidelberg (2012)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of boolean formulas. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol.\u00a07857, pp. 102\u2013117. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39611-3_14"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-31612-8_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"N. Manthey","year":"2012","unstructured":"Manthey, N.: Coprocessor 2.0: a flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 436\u2013441. Springer, Heidelberg (2012)"},{"key":"6_CR14","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (2009)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proc. 3rd Annual ACM Symposium on Theory of Computing, pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"key":"6_CR16","volume-title":"Stochastic Local Search","author":"H. Hoos","year":"2005","unstructured":"Hoos, H., St\u00fctzle, T.: Stochastic Local Search. Morgan Kaufmann \/ Elsevier, San Francisco (2005)"},{"issue":"2","key":"6_CR17","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/356586.356588","volume":"3","author":"E.G. Coffman","year":"1971","unstructured":"Coffman, E.G., Elphick, M., Shoshani, A.: System deadlocks. ACM Comput. Surv.\u00a03(2), 67\u201378 (1971)","journal-title":"ACM Comput. Surv."},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"issue":"1-4","key":"6_CR20","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10472-004-9433-0","volume":"43","author":"A. Gelder Van","year":"2005","unstructured":"Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence\u00a043(1-4), 239\u2013253 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"6_CR21","unstructured":"Lynce, I., Marques-Silva, J.: Probing-Based Preprocessing Techniques for Propositional Satisfiability. In: Proc. 15th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2003, pp. 105\u2013110 (2003)"},{"key":"6_CR22","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic","author":"G.S. Tseitin","year":"1970","unstructured":"Tseitin, G.S.: On the complexity of derivations in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125. Consultants Bureau, New York (1970)"},{"key":"6_CR23","unstructured":"Balint, A., Manthey, N.: Boosting the Performance of SLS and CDCL Solvers by Preprocessor Tuning. In: Pragmatics of SAT (POS 2013) (2013)"},{"key":"6_CR24","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: Wasito, I., Hasibuan, Z., Suhartanto, H. (eds.) Proc. of the International Conference on Advanced Computer Science and Information Systems, pp. 201\u2013206 (2001) ISBN 978-979-1421-11-9"},{"issue":"3","key":"6_CR25","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/s10601-012-9121-3","volume":"17","author":"R. Martins","year":"2012","unstructured":"Martins, R., Manquinho, V., Lynce, I.: An overview of parallel SAT solving. Constraints\u00a017(3), 304\u2013347 (2012)","journal-title":"Constraints"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Garey, M.R., Johnson, D.S., Stockmeyer, L.: Some simplified NP-complete problems. In: Proc. Sixth Annual ACM Symposium on Theory of Computing, STOC 1974, pp. 47\u201363 (1974)","DOI":"10.1145\/800119.803884"}],"container-title":["Lecture Notes in Computer Science","KI 2013: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40942-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T19:21:40Z","timestamp":1688412100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40942-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642409417","9783642409424"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40942-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}