{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:10:31Z","timestamp":1748664631421,"version":"3.41.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242453"},{"type":"electronic","value":"9783319242460"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_7","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"101-116","source":"Crossref","is-referenced-by-count":0,"title":["An Expressive Model for Instance Decomposition Based Parallel SAT Solvers"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Philipp","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"7_CR1","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":"7_CR2","first-page":"399","volume-title":"IJCAI 2009","author":"G. Audemard","year":"2009","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, pp. 399\u2013404. Morgan Kaufmann Publishers Inc., Pasadena (2009)"},{"issue":"1","key":"7_CR3","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 Intelligene Research\u00a022(1), 319\u2013351 (2004)","journal-title":"Journal of Artificial Intelligene Research"},{"key":"7_CR4","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":"7_CR5","unstructured":"Biere, A.: BooleForce and TraceCheck (2014). http:\/\/fmv.jku.at\/booleforce"},{"key":"7_CR6","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: Irwin, M.J. (ed.) DAC 1999, pp. 317\u2013320. ACM (1999)","DOI":"10.21236\/ADA360973"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Workshop SMT 2010, pp. 1\u20135. ACM (2009)","DOI":"10.1145\/1670412.1670413"},{"issue":"7","key":"7_CR8","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":"7_CR9","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":"7_CR10","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)"},{"key":"7_CR11","unstructured":"Gelder, A.V.: Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution. In: ISAIM 2002 (2002)"},{"key":"7_CR12","unstructured":"Gelder, A.V.: Verifying RUP proofs of propositional unsatisfiability. In: ISAIM 2008 (2008)"},{"key":"7_CR13","first-page":"10886","volume-title":"DATE 2003","author":"E. Goldberg","year":"2003","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE 2003, pp. 10886\u201310891. IEEE Computer Society, Washington, DC (2003)"},{"issue":"1\u20132","key":"7_CR14","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\u20132), 67\u2013100 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR15","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":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BFb0105407","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: St\u00e5lmarck\u2019s algorithm as a HOL derived rule. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 221\u2013234. Springer, Heidelberg (1996)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Heule, M., Manthey, N., Philipp, T.: Validating unsatisfiability results of clause sharing parallel SAT solvers. In: Berre, D.L. (ed.) POS 2014. EPiC Series, vol.\u00a027, pp. 12\u201325. EasyChair (2014)","DOI":"10.29007\/6vwg"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Jobstmann, B., Ray, S. (eds.) FMCAD 2013, pp. 181\u2013188. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"7_CR19","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":"7_CR20","first-page":"2318","volume-title":"IJCAI 2007","author":"J. Huang","year":"2007","unstructured":"Huang, J.: The effect of restarts on the efficiency of clause learning. In: Veloso, M. (ed.) IJCAI 2007, pp. 2318\u20132323. Morgan Kaufmann Publishers Inc., San Francisco (2007)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/11814948_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"A.E.J. Hyv\u00e4rinen","year":"2006","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T.A., Niemel\u00e4, I.: A distribution method for solving SAT in grids. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 430\u2013435. Springer, Heidelberg (2006)"},{"key":"7_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":"7_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-85776-1_21","volume-title":"Artificial Intelligence: Methodology, Systems, and Applications","author":"A.E.J. Hyv\u00e4rinen","year":"2008","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T.A., Niemel\u00e4, I.: Incorporating learning in grid-based randomized SAT solving. In: Dochev, D., Pistore, M., Traverso, P. (eds.) AIMSA 2008. LNCS (LNAI), vol.\u00a05253, pp. 247\u2013261. Springer, Heidelberg (2008)"},{"key":"7_CR24","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":"7_CR25","unstructured":"Irfan, A., Lanti, D., Manthey, N.: Modern cooperative parallel SAT solving. In: POS 2013 (2013)"},{"key":"7_CR26","series-title":"Department of Computer Science Series of Publications B","first-page":"64","volume-title":"Proceedings of SAT Challenge 2013","author":"A. Irfan","year":"2013","unstructured":"Irfan, A., Lanti, D., Manthey, N.: PCASSO a parallel cooperative sat SOlver. In: Balint, A., Belov, A., Heule, M.J.H., J\u00e4rvisalo, M. (eds.) Proceedings of SAT Challenge 2013. Department of Computer Science Series of Publications B, vol.\u00a0B-2013-1, pp. 64\u201365. University of Helsinki, Helsinki (2013)"},{"key":"7_CR27","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)"},{"key":"7_CR28","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":"7_CR29","doi-asserted-by":"crossref","unstructured":"Kautz, H.A., Selman, B.: Planning as satisfiability. In: Neumann, B. (ed.) ECAI 1992. pp. 359\u2013 363 (1992)","DOI":"10.1038\/359363a0"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-44973-4_6","volume-title":"Learning and Intelligent Optimization","author":"D. Lanti","year":"2013","unstructured":"Lanti, D., Manthey, N.: Sharing information in parallel search with search space partitioning. In: Nicosia, G., Pardalos, P. (eds.) LION 7. LNCS, vol.\u00a07997, pp. 52\u201358. Springer, Heidelberg (2013)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","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, pp. 136\u2013141. Springer, Heidelberg (2006)"},{"key":"7_CR32","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":"7_CR33","doi-asserted-by":"crossref","unstructured":"Manthey, N.: Towards Next Generation Sequential and Parallel SAT Solvers. Ph.D. thesis, Technische Universit\u00e4t Dresden, Informatik Fakult\u00e4t (2015)","DOI":"10.1007\/s10601-015-9226-6"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-39071-5_4","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"N. Manthey","year":"2013","unstructured":"Manthey, N., Philipp, T., Wernhard, C.: Soundness of inprocessing in clause sharing SAT solvers. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol.\u00a07962, pp. 22\u201339. Springer, Heidelberg (2013)"},{"issue":"1","key":"7_CR35","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/s10817-009-9127-8","volume":"43","author":"F. Mari\u0107","year":"2009","unstructured":"Mari\u0107, F.: Formalization and implementation of modern SAT solvers. Journal of Automated Reasoning\u00a043(1), 81\u2013119 (2009)","journal-title":"Journal of Automated Reasoning"},{"issue":"5","key":"7_CR36","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":"7_CR37","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":"7_CR38","first-page":"530","volume-title":"DAC 2001","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001, pp. 530\u2013535. Association for Computing Machinery, Las Vegas (2001)"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-27940-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Oe","year":"2012","unstructured":"Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: A verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 363\u2013378. Springer, Heidelberg (2012)"},{"key":"7_CR40","unstructured":"Philipp, T.: Expressive Models for Parallel Satisfiability Solvers. Master thesis, Technische Universit\u00e4t Dresden, Informatik Fakult\u00e4t (2013)"},{"key":"7_CR41","unstructured":": Engineering efficient planners with SAT. In: Raedt, L.D., Bessi\u00e8re, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) ECAI 2012. Frontiers in Artificial Intelligence and Applications, pp. 684\u2013689. IOS Press (2012)"},{"key":"7_CR42","first-page":"220","volume-title":"ICCAD 1996","author":"J.P.M. Silva","year":"1996","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD 1996, pp. 220\u2013227. IEEE Computer Society, Washington (1996)"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Singer, D.: Parallel resolution of the satisfiability problem: A survey. In: Talbi, E.G. (ed.) Parallel Combinatorial Optimization, chap. 5, pp. 123\u2013148. Wiley Interscience (2006)","DOI":"10.1002\/9780470053928.ch5"},{"key":"7_CR44","unstructured":"Soos, M.: CryptoMiniSat 2.5.0. In: SAT Race Competitive Event Booklet (2010)"},{"issue":"2","key":"7_CR45","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0004-3702(77)90029-7","volume":"9","author":"R.M. Stallman","year":"1977","unstructured":"Stallman, R.M., Sussman, G.J.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence\u00a09(2), 135\u2013196 (1977)","journal-title":"Artificial Intelligence"},{"key":"7_CR46","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: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"7_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N. Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol.\u00a08561, pp. 422\u2013429. Springer, Heidelberg (2014)"},{"key":"7_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-39634-2_18","volume-title":"Interactive Theorem Proving","author":"N. Wetzler","year":"2013","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 229\u2013244. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T18:26:27Z","timestamp":1748629587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}