{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T18:09:56Z","timestamp":1776881396381,"version":"3.51.2"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030242572","type":"print"},{"value":"9783030242589","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_9","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"136-154","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Incremental Inprocessing in SAT Solving"],"prefix":"10.1007","author":[{"given":"Katalin","family":"Fazekas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_23"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.artint.2016.08.007","volume":"241","author":"T Balyo","year":"2016","unstructured":"Balyo, T., Biere, A., Iser, M., Sinz, C.: SAT race 2015. Artif. Intell. 241, 45\u201365 (2016)","journal-title":"Artif. Intell."},{"key":"9_CR3","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. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"issue":"1&2","key":"9_CR4","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0743-1066(93)90018-C","volume":"15","author":"JN Hooker","year":"1993","unstructured":"Hooker, J.N.: Solving the incremental satisfiability problem. J. Log. Program. 15(1&2), 177\u2013186 (1993)","journal-title":"J. Log. Program."},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"issue":"4","key":"9_CR7","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543\u2013560 (2003)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"9_CR8","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10703-011-0122-4","volume":"39","author":"S Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Lewis, M.D.T., Schubert, T., Becker, B.: Incremental preprocessing methods for use in BMC. Form. Methods Syst. Des. 39(2), 185\u2013204 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Gocht, S., Balyo, T.: Accelerating SAT based planning with incremental SAT solving. In: Barbulescu, L., Frank, J., Mausam, Smith, S.F. (eds.) Proceedings of the 27th International Conference on Automated Planning and Scheduling, ICAPS 2017, pp. 135\u2013139. AAAI Press (2017)","DOI":"10.1609\/icaps.v27i1.13798"},{"key":"9_CR10","first-page":"59","volume":"9","author":"R Martins","year":"2014","unstructured":"Martins, R., Joshi, S., Manquinho, V.M., Lynce, I.: On using incremental encodings in unsatisfiability-based MaxSAT solving. JSAT 9, 59\u201381 (2014)","journal-title":"JSAT"},{"key":"9_CR11","unstructured":"Nadel, A.: Boosting minimal unsatisfiable core extraction. In: Bloem, R., Sharygina, N. (eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, pp. 221\u2013229. IEEE (2010)"},{"issue":"3\u20134","key":"9_CR12","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy satisability modulo theories. JSAT 3(3\u20134), 141\u2013224 (2007)","journal-title":"JSAT"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-24605-3_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"F Bacchus","year":"2004","unstructured":"Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 341\u2013355. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_26"},{"key":"9_CR14","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. 3569, pp. 61\u201375. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11499107_5"},{"key":"9_CR15","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":"MJH 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. 6695, pp. 201\u2013215. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_17"},{"key":"9_CR16","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. 6015, pp. 129\u2013144. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-14186-7_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 340\u2013345. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_30"},{"key":"9_CR19","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. 7317, pp. 256\u2013269. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_20"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-63046-5_9","volume-title":"Automated Deduction \u2013 CADE 26","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 130\u2013147. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_9"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. J. Autom. Reason. (2019). https:\/\/doi.org\/10.1007\/s10817-019-09516-0","DOI":"10.1007\/s10817-019-09516-0"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning sat solvers. In: Proceedings of the 24th AAAI Conference on Artificial Intelligence (AAAI 2010). AAAI Press (2010)","DOI":"10.1609\/aaai.v24i1.7553"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discret. Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discret. Appl. Math."},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-39611-3_14","volume-title":"Hardware and Software: Verification and Testing","author":"N Manthey","year":"2013","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. 7857, pp. 102\u2013117. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_14"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-09284-3_16","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"A Nadel","year":"2014","unstructured":"Nadel, A., Ryvchin, V., Strichman, O.: Ultimately incremental SAT. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 206\u2013218. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_16"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_19"},{"issue":"1\u20134","key":"9_CR27","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10817-018-9455-7","volume":"61","author":"JC Blanchette","year":"2018","unstructured":"Blanchette, J.C., Fleury, M., Lammich, P., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. J. Autom. Reason. 61(1\u20134), 333\u2013365 (2018)","journal-title":"J. Autom. Reason."},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-94205-6_10","volume-title":"Automated Reasoning","author":"K Fazekas","year":"2018","unstructured":"Fazekas, K., Bacchus, F., Biere, A.: Implicit hitting set algorithms for maximum satisfiability modulo theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 134\u2013151. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_10"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-319-09284-3_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"T Balyo","year":"2014","unstructured":"Balyo, T., Fr\u00f6hlich, A., Heule, M.J.H., Biere, A.: Everything you always wanted to know about blocked sets (but were afraid to ask). In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 317\u2013332. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_24"},{"key":"9_CR30","unstructured":"Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT competition 2014. In: Balint, A., Belov, A., Heule, M.J.H., J\u00e4rvisalo, M. (eds.) SAT Competition 2014. Department of Computer Science Series of Publications B, pp. 39\u201340. University of Helsinki (2014)"},{"issue":"3","key":"9_CR31","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.E.: A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett. 8(3), 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9_CR32","unstructured":"Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. In: Nebel, B. (ed.) Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001, Morgan Kaufmann, pp. 515\u2013522 (2001)"},{"key":"9_CR33","unstructured":"Biere, A.: CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT entering the SAT competition 2018. In: Heule, M.J.H., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2018 - Solver and Benchmark Descriptions. Volume B-2018-1 of Department of Computer Science Series of Publications B, pp. 13\u201314. University of Helsinki (2018)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Luo, M., Li, C., Xiao, F., Many\u00e0, F., L\u00fc, Z.: An effective learnt clause minimization approach for CDCL SAT solvers. In: Sierra, C. (ed.) Proceedings of the 26th International Joint Conference on Artificial Intelligence, IJCAI 2017, pp. 703\u2013711. ijcai.org (2017)","DOI":"10.24963\/ijcai.2017\/98"},{"key":"9_CR35","unstructured":"Piette, C., Hamadi, Y., Sais, L.: Vivifying propositional clausal formulae. In: Ghallab, M., Spyropoulos, C.D., Fakotakis, N., Avouris, N.M. (eds.) Proceedings of the 18th European Conference on Artificial Intelligence, ECAI 2008. Volume 178 of Frontiers in Artificial Intelligence and Applications, pp. 525\u2013529. IOS Press (2008)"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Schwartz, E.J., Avgerinos, T., Brumley, D.: All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In: 31st IEEE Symposium on Security and Privacy, S&P 2010, 16\u201319 May 2010, pp. 317\u2013331. IEEE Computer Society, Berleley\/Oakland (2010)","DOI":"10.1109\/SP.2010.26"},{"key":"9_CR37","unstructured":"Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Technical report, FMV reports series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2011)"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Biere, A., van Dijk, T., Heljanko, K.: Hardware model checking competition 2017. In: Stewart, D., Weissenbacher, G. (eds.) Formal Methods in Computer Aided Design, FMCAD 2017, p. 9. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102233"},{"issue":"3","key":"9_CR39","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electr. Notes Theor. Comput. Sci. 174(3), 45\u201356 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-38171-3_6","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"MJH Heule","year":"2013","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Revisiting hyper binary resolution. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 77\u201393. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38171-3_6"},{"issue":"12","key":"9_CR41","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans CAD Integr. Circ. Syst. 21(12), 1377\u20131394 (2002)","journal-title":"IEEE Trans CAD Integr. Circ. Syst."},{"key":"9_CR42","unstructured":"Brummayer, R., Biere, A.: Local two-level and-inverter graph minimization without blowup. In: Proceedings of the 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006) (2006)"},{"key":"9_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-319-96145-3_32","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector\u00a03.0. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 587\u2013595. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_32"},{"key":"9_CR44","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M. (eds.): Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions. Volume B-2016-1 of Department of Computer Science Series of Publications B. University of Helsinki (2016)"},{"key":"9_CR45","unstructured":"Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M., (eds.): Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions. Volume B-2017-1 of Department of Computer Science Series of Publications B. University of Helsinki (2017)"},{"key":"9_CR46","unstructured":"Audemard, G., Simon, L.: Glucose and syrup in the SAT 2017. In: Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M. (eds.) Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions. Volume B-2017-1 of Department of Computer Science Series of Publications B, pp. 16\u201317. University of Helsinki (2017)"},{"key":"9_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"},{"key":"9_CR48","unstructured":"Manthey, N.: Riss 7. In Balyo, T., Heule, M.J.H., J\u00e4rvisalo, M., (eds.) Proceedings of SAT Competition 2017 - Solver and Benchmark Descriptions. Volume B-2017-1 of Department of Computer Science Series of Publications B, p. 29. University of Helsinki (2017)"},{"key":"9_CR49","doi-asserted-by":"crossref","unstructured":"Han, H., Somenzi, F.: Alembic: an efficient algorithm for CNF preprocessing. In: Proceedings of the 44th Design Automation Conference, DAC 2007, pp. 582\u2013587. IEEE (2007)","DOI":"10.1109\/DAC.2007.375231"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,17]],"date-time":"2023-09-17T21:21:31Z","timestamp":1694985691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}