{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T18:16:45Z","timestamp":1725733005165},"publisher-location":"Berlin, Heidelberg","reference-count":45,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642390708"},{"type":"electronic","value":"9783642390715"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39071-5_4","type":"book-chapter","created":{"date-parts":[[2013,6,24]],"date-time":"2013-06-24T01:23:17Z","timestamp":1372036997000},"page":"22-39","source":"Crossref","is-referenced-by-count":4,"title":["Soundness of Inprocessing in Clause Sharing SAT\u00a0Solvers"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Manthey","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Philipp","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Wernhard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-31612-8_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"G. Audemard","year":"2012","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.-M., Piette, C.: Revisiting clause exchange in parallel SAT solving. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 200\u2013213. Springer, Heidelberg (2012)"},{"key":"#cr-split#-4_CR2.1","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Lagniez, J.M., Piette, C.: Penelope, a parallel clause-freezer solver. In: SAT Challenge 2012"},{"key":"#cr-split#-4_CR2.2","unstructured":"Solver and Benchmark Descriptions, pp. 43-44 (2012)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-21581-0_16","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"G. Audemard","year":"2011","unstructured":"Audemard, G., Lagniez, J.-M., Mazure, B., Sa\u00efs, L.: On freezing and reactivating learnt clauses. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 188\u2013200. Springer, Heidelberg (2011)"},{"key":"4_CR4","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. Morgan Kaufmann (2009)"},{"issue":"1","key":"4_CR5","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research\u00a022(1), 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"4_CR6","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10\/1, Johannes Kepler University, Linz, Austria (2010)"},{"key":"4_CR7","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: Proc. 36th Annual ACM\/IEEE Design Automation Conf (DAC), pp. 317\u2013320. ACM (1999)","DOI":"10.1145\/309847.309942"},{"key":"4_CR8","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M. B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A fast parallel SAT-solver \u2013 efficient workload balancing. Annals of Mathematics and Artificial Intelligence 17, 381\u2013400 (1996), (Based on a technical report published already in 1994)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"7","key":"4_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. CACM\u00a05(7), 394\u2013397 (1962)","journal-title":"CACM"},{"key":"4_CR10","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":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","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, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A.V. Gelder","year":"2005","unstructured":"Gelder, A.V.: Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence\u00a043(1), 239\u2013253 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"1-2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"C.P. Gomes","year":"2000","unstructured":"Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of Automated Reasoning\u00a024(1-2), 67\u2013100 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR14","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":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-15396-9_22","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"L. Guo","year":"2010","unstructured":"Guo, L., Hamadi, Y., Jabbour, S., Sais, L.: Diversification and intensification in parallel SAT solving. In: Cohen, D. (ed.) CP 2010. LNCS, vol.\u00a06308, pp. 252\u2013265. Springer, Heidelberg (2010)"},{"issue":"4","key":"4_CR16","first-page":"127","volume":"7","author":"Y. Hamadi","year":"2011","unstructured":"Hamadi, Y., Jabbour, S., Piette, C., Sais, L.: Deterministic parallel DPLL. JSAT\u00a07(4), 127\u2013132 (2011)","journal-title":"JSAT"},{"key":"4_CR17","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Control-based clause sharing in parallel SAT solving. In: Proc. 21st Int. Joint Conf. on Artificial Intelligence (IJCAI 2009), pp. 499\u2013504 (2009)"},{"issue":"4","key":"4_CR18","first-page":"245","volume":"6","author":"Y. Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. JSAT\u00a06(4), 245\u2013262 (2009)","journal-title":"JSAT"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"M.J.H. Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol.\u00a07261, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-21581-0_17","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M.J.H. Heule","year":"2011","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Efficient CNF simplification based on binary implication graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 201\u2013215. Springer, Heidelberg (2011)"},{"key":"4_CR21","unstructured":"H\u00f6lldobler, S., Manthey, N., Nguyen, V., Stecklina, J., Steinke, P.: A short overview on modern parallel SAT-solvers. In: Proc. Int. Conf. on Advanced Computer Science and Information Systems (ICACSIS 2011), pp. 201\u2013206. IEEE (2011)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-16242-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A.E.J. Hyv\u00e4rinen","year":"2010","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Partitioning SAT instances for distributed solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 372\u2013386. Springer, Heidelberg (2010)"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-31612-8_17","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A.E.J. Hyv\u00e4rinen","year":"2012","unstructured":"Hyv\u00e4rinen, A.E.J., Manthey, N.: Designing scalable parallel SAT solvers. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 214\u2013227. Springer, Heidelberg (2012)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-642-23786-7_30","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2011","author":"A.E.J. Hyv\u00e4rinen","year":"2011","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: Grid-based SAT solving with iterative partitioning and clause learning. In: Lee, J. (ed.) CP 2011. LNCS, vol.\u00a06876, pp. 385\u2013399. Springer, Heidelberg (2011)"},{"key":"4_CR25","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.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M. J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-21581-0_27","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"H. Katebi","year":"2011","unstructured":"Katebi, H., Sakallah, K.A., Marques-Silva, J.P.: Empirical study of the anatomy of modern SAT solvers. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 343\u2013356. Springer, Heidelberg (2011)"},{"issue":"1","key":"4_CR28","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"97","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96-\u00a097(1), 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics 96-"},{"key":"4_CR29","unstructured":"Lanti, D., Manthey, N.: Sharing information in parallel search with search space partitioning. In: Learning and Intelligent Optimization \u2013 7th Int. Conf. (LION 7) (to appear, 2013)"},{"key":"4_CR30","unstructured":"Lynce, I., Marques-Silva, J.P.: Probing-based preprocessing techniques for propositional satisfiability. In: Proc. 15th IEEE Int. Conf. on Tools with Artificial Intelligence (ICTAI 2003), pp. 105\u2013110. IEEE (2003)"},{"key":"4_CR31","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 \u2013 A flexible CNF simplifier. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 436\u2013441. Springer, Heidelberg (2012)"},{"key":"4_CR32","unstructured":"Manthey, N., Heule, M.J.H., Biere, A.: Automated reencoding of Boolean formulas. In: Hardware and Software: Verification and Testing \u2013 8th Int. Haifa Verification Conf. (HVC 2012). LNCS, Springer (to appear, 2013)"},{"issue":"5","key":"4_CR33","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"4_CR34","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":"4_CR35","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 ACM\/IEEE Design Automation Conf. (DAC), pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"4_CR36","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1016\/j.artint.2010.10.002","volume":"175","author":"K. Pipatsrisawat","year":"2011","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence\u00a0175(2), 512\u2013525 (2011)","journal-title":"Artificial Intelligence"},{"key":"4_CR37","unstructured":"Roussel, O.: Description of ppfolio 2012. In: Proc. SAT Challenge 2012; Solver and Benchmark Descriptions, p. 46. Univ. of Helsinki (2012), \n                    \n                      http:\/\/hdl.handle.net\/10138\/34218"},{"key":"4_CR38","unstructured":"Soos, M.: Cryptominisat 2.5.0. In: SAT Race Competitive Event Booklet (July 2010), \n                    \n                      http:\/\/baldur.iti.uka.de\/sat-race-2010\/descriptions\/solver_13.pdf\n                    \n                    \n                   (retrieved February 11, 2013)"},{"key":"4_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-02777-2_23","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"N. S\u00f6rensson","year":"2009","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 237\u2013243. Springer, Heidelberg (2009)"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Subbarayan","year":"2005","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivations in the propositional calculus. Studies in Mathematics and Mathematical Logic Part II, 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"#cr-split#-4_CR42.1","unstructured":"Wotzlaw, A., van der Grinten, A., Speckenmeyer, E., Porschen, S.: pfoliouzk: Solver description. In: Proc. SAT Challenge 2012"},{"key":"#cr-split#-4_CR42.2","unstructured":"Solver and Benchmark Descriptions, p. 45. Univ. of Helsinki (2012),     http:\/\/hdl.handle.net\/10138\/34218"},{"issue":"4","key":"4_CR43","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H. Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: Psato: a distributed propositional prover and its application to quasigroup problems. Journal of Symbolic Computation\u00a021(4), 543\u2013560 (1996)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2013"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39071-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T14:11:59Z","timestamp":1557843119000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39071-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390708","9783642390715"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39071-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}