{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:04:39Z","timestamp":1779087879624,"version":"3.51.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030802226","type":"print"},{"value":"9783030802233","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-80223-3_37","type":"book-chapter","created":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T14:13:49Z","timestamp":1625148829000},"page":"545-561","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Logical Cryptanalysis with WDSat"],"prefix":"10.1007","author":[{"given":"Monika","family":"Trimoska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Dequen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sorina","family":"Ionica","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,2]]},"reference":[{"key":"37_CR1","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11\u201317, 2009, pp. 399\u2013404 (2009)"},{"issue":"3","key":"37_CR2","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1515\/JMC.2009.009","volume":"3","author":"L Bettale","year":"2009","unstructured":"Bettale, L., Faug\u00e8re, J., Perret, L.: Hybrid approach for solving multivariate systems over finite fields. J. Math. Cryptol. 3(3), 177\u2013197 (2009)","journal-title":"J. Math. Cryptol."},{"key":"37_CR3","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT competition 2020. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 51\u201353. University of Helsinki (2020)"},{"key":"37_CR4","unstructured":"Bouillaguet, C.: LibFES-lite. https:\/\/github.com\/cbouilla\/libfes-lite (2016)"},{"key":"37_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-662-43414-7_11","volume-title":"Selected Areas in Cryptography \u2013 SAC 2013","author":"C Bouillaguet","year":"2014","unstructured":"Bouillaguet, C., Cheng, C.-M., Chou, T., Niederhagen, R., Yang, B.-Y.: Fast exhaustive search for quadratic systems in $$\\mathbb{F}_{2}$$ on FPGAs. In: Lange, T., Lauter, K., Lison\u011bk, P. (eds.) SAC 2013. LNCS, vol. 8282, pp. 205\u2013222. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43414-7_11"},{"key":"37_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/3-540-45539-6_27","volume-title":"Advances in Cryptology \u2014 EUROCRYPT 2000","author":"N Courtois","year":"2000","unstructured":"Courtois, N., Klimov, A., Patarin, J., Shamir, A.: Efficient algorithms for solving overdefined systems of multivariate polynomial equations. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 392\u2013407. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45539-6_27"},{"issue":"7","key":"37_CR7","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.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"37_CR8","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\u20133","key":"37_CR9","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/S0022-4049(99)00005-5","volume":"139","author":"JC Faug\u00e8re","year":"1999","unstructured":"Faug\u00e8re, J.C.: A new efficient algorithm for computing Gr\u00f6bner basis (F4). J. Pure Appl. Algebra 139(1\u20133), 61\u201388 (1999)","journal-title":"J. Pure Appl. Algebra"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-319-13039-2_24","volume-title":"Progress in Cryptology \u2013 INDOCRYPT 2014","author":"SD Galbraith","year":"2014","unstructured":"Galbraith, S.D., Gebregiyorgis, S.W.: Summation polynomial algorithms for elliptic curves in characteristic two. In: Meier, W., Mukhopadhyay, D. (eds.) INDOCRYPT 2014. LNCS, vol. 8885, pp. 409\u2013427. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13039-2_24"},{"key":"37_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-642-31424-7_31","volume-title":"Computer Aided Verification","author":"C-S Han","year":"2012","unstructured":"Han, C.-S., Jiang, J.-H.R.: When Boolean satisfiability meets Gaussian elimination in a simplex way. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 410\u2013426. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_31"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11527695_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"M Heule","year":"2005","unstructured":"Heule, M., Dufour, M., van Zwieten, J., van Maaren, H.: March_eq: implementing additional reasoning into an efficient look-ahead SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 345\u2013359. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11527695_26"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-76620-1_1","volume-title":"Number-Theoretic Methods in Cryptology","author":"A Joux","year":"2018","unstructured":"Joux, A., Vitse, V.: A crossbred algorithm for solving Boolean polynomial systems. In: Kaczorowski, J., Pieprzyk, J., Pomyka\u0142a, J. (eds.) NuTMiC 2017. LNCS, vol. 10737, pp. 3\u201321. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-76620-1_1"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-31612-8_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"T Laitinen","year":"2012","unstructured":"Laitinen, T., Junttila, T., Niemel\u00e4, I.: Conflict-driven XOR-clause learning. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 383\u2013396. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_29"},{"key":"37_CR15","unstructured":"van Maaren, H., Franco, J.: The International SAT Competition Web Page. http:\/\/www.satcompetition.org\/. Accessed 27 May 2020"},{"key":"37_CR16","doi-asserted-by":"crossref","unstructured":"Macaulay, F.S.: The Algebraic Theory of Modular Systems. Cambridge Tracts in Mathematics and Mathematical Physics, University Press (1916). https:\/\/books.google.fr\/books?id=uA7vAAAAMAAJ","DOI":"10.3792\/chmm\/1263317740"},{"key":"37_CR17","doi-asserted-by":"crossref","unstructured":"Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reasoning 24(1\/2), 165\u2013203 (2000), http:\/\/dblp.uni-trier.de\/db\/journals\/jar\/jar24.html#MassacciM00","DOI":"10.1023\/A:1006326723002"},{"key":"37_CR18","unstructured":"McDonald, C., Charnes, C., Pieprzyk, J.: An algebraic analysis of Trivium ciphers based on the Boolean satisfiability problem. IACR Cryptol. ePrint Arch. 2007, 129 (2007). http:\/\/eprint.iacr.org\/2007\/129"},{"key":"37_CR19","unstructured":"Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: POS-10. Pragmatics of SAT, Edinburgh, UK, July 10, 2010. EPiC Series in Computing, vol. 8, pp. 2\u201314. EasyChair (2010)"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Soos, M., Meel, K.S.: BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, 27 January\u20131 February 2019, pp. 1592\u20131599. AAAI Press (2019)","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"37_CR21","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":"37_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"774","DOI":"10.1007\/978-3-030-58475-7_45","volume-title":"Principles and Practice of Constraint Programming","author":"M Trimoska","year":"2020","unstructured":"Trimoska, M., Ionica, S., Dequen, G.: Parity (XOR) reasoning for the index calculus attack. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 774\u2013790. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_45"},{"key":"37_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-030-51938-4_11","volume-title":"Progress in Cryptology - AFRICACRYPT 2020","author":"M Trimoska","year":"2020","unstructured":"Trimoska, M., Ionica, S., Dequen, G.: A SAT-based approach for index calculus on binary elliptic curves. In: Nitaj, A., Youssef, A. (eds.) AFRICACRYPT 2020. LNCS, vol. 12174, pp. 214\u2013235. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51938-4_11"},{"key":"37_CR24","unstructured":"Zhang, X., Cai, S.: Relaxed backtracking with Rephasing. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proceedings of SAT Competition 2020 - Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2020-1, pp. 16\u201317. University of Helsinki (2020)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2021"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-80223-3_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,1]],"date-time":"2021-07-01T23:37:18Z","timestamp":1625182638000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-80223-3_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030802226","9783030802233"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-80223-3_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 July 2021","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":"Barcelona","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.iiia.csic.es\/sat2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}