{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:27:39Z","timestamp":1725863259054},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319449524"},{"type":"electronic","value":"9783319449531"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-44953-1_3","type":"book-chapter","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T15:12:23Z","timestamp":1471878743000},"page":"30-48","source":"Crossref","is-referenced-by-count":12,"title":["An Adaptive Parallel SAT Solver"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Audemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Marie","family":"Lagniez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Szczepanski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u00e9bastien","family":"Tabary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,23]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 7317, pp. 200\u2013213. Springer, Heidelberg (2012)"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Audemard, G., Hoessen, B., Jabbour, S., Piette, C.: An effective distributed d&c approach for the satisfiability problem. In: 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, Torino, Italy, pp. 183\u2013187, 12\u201314 February 2014","DOI":"10.1109\/PDP.2014.92"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6695, pp. 188\u2013200. Springer, Heidelberg (2011)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/978-3-642-39071-5_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"G Audemard","year":"2013","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309\u2013317. Springer, Heidelberg (2013)"},{"key":"3_CR5","unstructured":"Audemard, G., Lagniez, J.-M., Simon, L.: Just-in-time compilation of knowledge bases. In: Proceedings of the 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013, Beijing, China, 3\u20139 August 2013"},{"key":"3_CR6","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, pp. 399\u2013404, 11\u201317 July 2009"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Heidelberg (2014)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-24318-4_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"T Balyo","year":"2015","unstructured":"Balyo, T., Sanders, P., Sinz, C.: HordeSat: a massively parallel portfolio SAT solver. In: Heule, M. (ed.) SAT 2015. LNCS, vol. 9340, pp. 156\u2013172. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24318-4_12"},{"issue":"2","key":"3_CR9","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"3_CR10","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","year":"2009","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"3_CR11","unstructured":"Biere, A.: Bounded model checking. In: Biere et al. [10], Chap. 14, vol. 185, pp. 455\u2013481, February 2009"},{"key":"3_CR12","unstructured":"Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, p. 51 (2013)"},{"key":"3_CR13","unstructured":"Biere, A.: Yet another local search solver and lingeling and friends entering the sat competition 2014. In: Proceedings of SAT Competition (2014)"},{"key":"3_CR14","unstructured":"Chen, J.: Minisat bcd and abcdsat: solvers based on blocked clause decomposition. In: SAT RACE 2015 Solvers Description (2015)"},{"issue":"6","key":"3_CR15","doi-asserted-by":"crossref","first-page":"795","DOI":"10.1002\/cpe.1079","volume":"19","author":"W Chrabakh","year":"2007","unstructured":"Chrabakh, W., Wolski, R.: The gridsat portal: a grid web-based portal for solving satisfiability problems using the national cyberinfrastructure. Concurrency Comput. Pract. Exp. 19(6), 795\u2013808 (2007)","journal-title":"Concurrency Comput. Pract. Exp."},{"key":"3_CR16","unstructured":"Chu, G., Stuckey, P.J., Harwood, A.: Pminisat: a parallelization of minisat 2.0. Technical report, SAT Race (2008)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"issue":"3","key":"3_CR18","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.entcs.2004.10.020","volume":"128","author":"Y Feldman","year":"2005","unstructured":"Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: design and implementation. Electron. Notes Theoret. Comput. Sci. 128(3), 75\u201390 (2005)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"issue":"12","key":"3_CR19","doi-asserted-by":"crossref","first-page":"1549","DOI":"10.1016\/j.dam.2006.10.007","volume":"155","author":"E Goldberg","year":"2007","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: a fast and robust sat-solver. Discrete Appl. Math. 155(12), 1549\u20131561 (2007)","journal-title":"Discrete Appl. Math."},{"key":"3_CR20","unstructured":"Gomes, C.P., Selman, B., Kautz, H.A.: Boosting combinatorial search through randomization. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 1998, IAAI 1998, Madison, Wisconsin, USA, pp. 431\u2013437, 26\u201330 July 1998"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6308, pp. 252\u2013265. Springer, Heidelberg (2010)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Guo, L., Lagniez, J.-M.: Dynamic polarity adjustment in a parallel SAT solver. In: IEEE 23rd International Conference on Tools with Artificial Intelligence, ICTAI 2011, Boca Raton, FL, USA, pp. 67\u201373, 7\u20139 November 2011","DOI":"10.1109\/ICTAI.2011.19"},{"key":"3_CR23","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Control-based clause sharing in parallel SAT solving. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, Pasadena, California, USA, pp. 499\u2013504, 11\u201317 July 2009"},{"issue":"4","key":"3_CR24","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. JSAT 6(4), 245\u2013262 (2009)","journal-title":"JSAT"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH 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. 7261, pp. 50\u201365. Springer, Heidelberg (2012)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/978-3-642-16242-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"AEJ 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. 6397, pp. 372\u2013386. Springer, Heidelberg (2010)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/978-3-642-39071-5_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"J-M Lagniez","year":"2013","unstructured":"Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276\u2013292. Springer, Heidelberg (2013)"},{"key":"3_CR29","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S1571-0653(04)00314-2","volume":"9","author":"D Le Berre","year":"2001","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead. Electron. Notes Discrete Math. 9, 59\u201380 (2001)","journal-title":"Electron. Notes Discrete Math."},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP - a new search algorithm for satisfiability. In: Proceedings of the 1996 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1996, pp. 220\u2013227 (1996)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Martins, R., Manquinho, V.M., Lynce, I.: Improving search space splitting for parallel SAT solving. In: 22nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2010, Arras, France, vol. 1, pp. 336\u2013343, 27\u201329 October 2010","DOI":"10.1109\/ICTAI.2010.56"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, pp. 530\u2013535. ACM, 18\u201322 June 2001","DOI":"10.1145\/378239.379017"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-642-31612-8_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Nadel","year":"2012","unstructured":"Nadel, A., Ryvchin, V.: Efficient SAT solving under assumptions. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 242\u2013255. Springer, Heidelberg (2012)"},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K Pipatsrisawat","year":"2007","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. 4501, pp. 294\u2013299. Springer, Heidelberg (2007)"},{"key":"3_CR35","unstructured":"Rintanen, J.: Planning and SAT. In: Biere et al. [10], Chap. 15, vol. 185, pp. 483\u2013504, February 2009"},{"key":"3_CR36","unstructured":"Roussel, O.: ppfolio. http:\/\/www.cril.univ-artois.fr\/~roussel\/ppfolio"},{"key":"3_CR37","unstructured":"SAT-race (2015). http:\/\/baldur.iti.kit.edu\/sat-race-2015\/"},{"issue":"4","key":"3_CR38","doi-asserted-by":"crossref","first-page":"203","DOI":"10.3233\/SAT190068","volume":"6","author":"T Schubert","year":"2009","unstructured":"Schubert, T., Lewis, M., Becker, B.: Pamiraxt: parallel SAT solving with threads and message passing. J. Satisfiability Boolean Model. Comput. 6(4), 203\u2013222 (2009)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-319-21909-7_21","volume-title":"Parallel Computing Technologies","author":"A Semenov","year":"2015","unstructured":"Semenov, A., Zaikin, O.: Using monte carlo method for searching partitionings of hard variants of boolean satisfiability problem. In: Malyshkin, V. (ed.) PaCT 2015. LNCS, vol. 9251, pp. 222\u2013230. Springer, Heidelberg (2015)"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009)"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/978-3-642-31612-8_42","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"P Tak van der","year":"2012","unstructured":"van der Tak, P., Heule, M.J.H., Biere, A.: Concurrent cube-and-conquer. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 475\u2013476. Springer, Heidelberg (2012)"},{"issue":"4","key":"3_CR42","doi-asserted-by":"crossref","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. J. Symbolic Comput. 21(4), 543\u2013560 (1996)","journal-title":"J. Symbolic Comput."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-44953-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,25]],"date-time":"2020-09-25T11:59:35Z","timestamp":1601035175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-44953-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319449524","9783319449531"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-44953-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}