{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:19:59Z","timestamp":1772119199095,"version":"3.50.1"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T00:00:00Z","timestamp":1711411200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T00:00:00Z","timestamp":1711411200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"Huawei","award":["TC20211214628"],"award-info":[{"award-number":["TC20211214628"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2024,10]]},"DOI":"10.1007\/s00224-024-10168-w","type":"journal-article","created":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T02:14:30Z","timestamp":1711419270000},"page":"1291-1311","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["CNF Encodings of Symmetric Functions"],"prefix":"10.1007","volume":"68","author":[{"given":"Gregory","family":"Emdin","sequence":"first","affiliation":[]},{"given":"Alexander S.","family":"Kulikov","sequence":"additional","affiliation":[]},{"given":"Ivan","family":"Mihajlin","sequence":"additional","affiliation":[]},{"given":"Nikita","family":"Slezkin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,3,26]]},"reference":[{"issue":"1","key":"10168_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1137\/060664537","volume":"38","author":"E Allender","year":"2008","unstructured":"Allender, E., Hellerstein, L., McCabe, P., Pitassi, T., Saks, M.E.: Minimizing disjunctive normal form formulas and $$\\mathit{AC}^0$$ circuits given a truth table. SIAM J. Comput. 38(1), 63\u201384 (2008). https:\/\/doi.org\/10.1137\/060664537","journal-title":"SIAM J. Comput."},{"key":"10168_CR2","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming - CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient cnf encoding of boolean cardinality constraints. In: Rossi, F. (ed.) Principles and Practice of Constraint Programming - CP 2003, pp. 108\u2013122. Heidelberg, Springer, Berlin Heidelberg, Berlin (2003)"},{"key":"10168_CR3","doi-asserted-by":"publisher","unstructured":"Bittner, P.M., Th\u00fcm, T., Schaefer, I.: SAT encodings of the at-most-k constraint - A case study on configuring university courses. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings, volume 11724 of Lecture Notes in Computer Science, pp. 127\u2013144. Springer, (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_7","DOI":"10.1007\/978-3-030-30446-1_7"},{"issue":"1","key":"10168_CR4","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1023\/A:1009812409930","volume":"4","author":"B Cabon","year":"1999","unstructured":"Cabon, B., de Givry, S., Lobjois, L., Schiex, T., Warners, J.P.: Radio link frequency assignment. Constraints An Int. J. 4(1), 79\u201389 (1999). https:\/\/doi.org\/10.1023\/A:1009812409930","journal-title":"Constraints An Int. J."},{"issue":"7","key":"10168_CR5","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1016\/j.ipl.2010.01.007","volume":"110","author":"E Demenkov","year":"2010","unstructured":"Demenkov, E., Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: New upper bounds on the boolean circuit complexity of symmetric functions. Inf. Process. Lett. 110(7), 264\u2013267 (2010). https:\/\/doi.org\/10.1016\/j.ipl.2010.01.007","journal-title":"Inf. Process. Lett."},{"key":"10168_CR6","doi-asserted-by":"publisher","unstructured":"Emdin, G., Kulikov, A.S., Mihajlin, I., Slezkin, N.: CNF Encodings of Parity. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022), volume 241 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 47:1\u201347:12, Dagstuhl, Germany, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.MFCS.2022.47, https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.47","DOI":"10.4230\/LIPIcs.MFCS.2022.47"},{"key":"10168_CR7","unstructured":"Frisch, A.M., Giannaros, P.A.: SAT encodings of the at-most-$$k$$ constraint: Some old, some new, some fast, some slow. In: Proceedings of the 9th International Workshop on Constraint Modelling and Reformulation (2010)"},{"key":"10168_CR8","doi-asserted-by":"publisher","unstructured":"H\u00e5stad, J.: Almost optimal lower bounds for small depth circuits. In: Hartmanis, J. (ed.) Proceedings of the 18th Annual ACM Symposium on Theory of Computing, May 28-30, 1986, Berkeley, California, USA, pp. 6\u201320. ACM, (1986). https:\/\/doi.org\/10.1145\/12130.12132","DOI":"10.1145\/12130.12132"},{"key":"10168_CR9","doi-asserted-by":"publisher","unstructured":"H\u00e5stad, J., Jukna, S., Pudl\u00e1k, P.: Top-down lower bounds for depth 3 circuits. In: 34th Annual Symposium on Foundations of Computer Science, Palo Alto, California, USA, 3\u20135 November 1993, pp. 124\u2013129. IEEE Computer Society, (1993). https:\/\/doi.org\/10.1109\/SFCS.1993.366875","DOI":"10.1109\/SFCS.1993.366875"},{"key":"10168_CR10","unstructured":"Hirahara, S.: A duality between depth-three formulas and approximation by depth-two. Electron. Colloquium Comput. Complex., pp. 92, (2017). https:\/\/eccc.weizmann.ac.il\/report\/2017\/092"},{"key":"10168_CR11","doi-asserted-by":"publisher","unstructured":"Hrube\u0161, P., Natarajan\u00a0Ramamoorthy, S., Rao, A., Yehudayoff, A.: Lower Bounds on Balancing Sets and Depth-2 Threshold Circuits. In: Baier, C., Chatzigiannakis, I., Flocchini, P., Leonardi, S. (eds.) 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 72:1\u201372:14, Dagstuhl, Germany, Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ICALP.2019.72, https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2019.72","DOI":"10.4230\/LIPIcs.ICALP.2019.72"},{"key":"10168_CR12","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: Pysat: A python toolkit for prototyping with sat oracles. In: International Conference on Theory and Applications of Satisfiability Testing, (2018)","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"10168_CR13","doi-asserted-by":"publisher","unstructured":"Jukna, S.: Boolean Function Complexity - Advances and Frontiers, vol. 27 of Algorithms and combinatorics. Springer, (2012). https:\/\/doi.org\/10.1007\/978-3-642-24508-4","DOI":"10.1007\/978-3-642-24508-4"},{"key":"10168_CR14","doi-asserted-by":"publisher","unstructured":"Klawe, M., Paul, W.J., Pippenger, N., Yannakakis, M.: On monotone formulae with restricted depth. In: Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, STOC \u201984, pp. 480\u2013487, New York, NY, USA, Association for Computing Machinery (1984). https:\/\/doi.org\/10.1145\/800057.808717","DOI":"10.1145\/800057.808717"},{"key":"10168_CR15","unstructured":"Kochemazov, S., Zaikin, O., Semenov, A.: The comparison of different sat encodings for the problem of search for systems of orthogonal latin squares. In: International Conference Mathematical and Information Technologies-MIT, pp. 155\u2013165, (2016)"},{"key":"10168_CR16","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.tcs.2018.09.003","volume":"762","author":"P Kucera","year":"2019","unstructured":"Kucera, P., Savick\u00fd, P., Vorel, V.: A lower bound on CNF encodings of the at-most-one constraint. Theor. Comput. Sci. 762, 51\u201373 (2019). https:\/\/doi.org\/10.1016\/j.tcs.2018.09.003","journal-title":"Theor. Comput. Sci."},{"key":"10168_CR17","doi-asserted-by":"publisher","unstructured":"Kuechlin, W., Sinz, C.: Proving consistency assertions for automotive product data management. J. Autom. Reasoning 24, 145\u2013163 02 (2000). https:\/\/doi.org\/10.1023\/A:1006370506164","DOI":"10.1023\/A:1006370506164"},{"key":"10168_CR18","unstructured":"Li, C.-M.: Integrating equivalency reasoning into davis-putnam procedure. 04 (2000)"},{"key":"10168_CR19","doi-asserted-by":"publisher","unstructured":"Li, J., Yang, T.: 3.1n - o(n) circuit lower bounds for explicit functions. In: Leonardi, S., Gupta, A. (eds.) STOC \u201922: 54th Annual ACM SIGACT Symposium on Theory of Computing, Rome, Italy, June 20 - 24, 2022, pp. 1180\u20131193. ACM, (2022). https:\/\/doi.org\/10.1145\/3519935.3519976","DOI":"10.1145\/3519935.3519976"},{"key":"10168_CR20","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-74970-7_35","volume-title":"Principles and Practice of Constraint Programming - CP 2007","author":"J Marques-Silva","year":"2007","unstructured":"Marques-Silva, J., Lynce, I.: Towards robust cnf encodings of cardinality constraints. In: Bessi\u00e8re, C. (ed.) Principles and Practice of Constraint Programming - CP 2007, pp. 483\u2013497. Heidelberg, Springer, Berlin Heidelberg, Berlin (2007)"},{"key":"10168_CR21","unstructured":"Masek, W.J.: Some NP-complete set covering problems. Unpublished Manuscript (1979)"},{"key":"10168_CR22","unstructured":"Paturi, R., Pudl\u00e1k, P., Zane, F.: Satisfiability coding lemma. Chic. J. Theor. Comput. Sci. 1999 (1999). http:\/\/cjtcs.cs.uchicago.edu\/articles\/1999\/11\/contents.html"},{"issue":"2","key":"10168_CR23","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0166-218X(02)00410-9","volume":"130","author":"SD Prestwich","year":"2003","unstructured":"Prestwich, S.D.: SAT problems with chains of dependent variables. Discret. Appl. Math. 130(2), 329\u2013350 (2003). https:\/\/doi.org\/10.1016\/S0166-218X(02)00410-9","journal-title":"Discret. Appl. Math."},{"key":"10168_CR24","doi-asserted-by":"publisher","unstructured":"Prestwich, S.D.: CNF encodings. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, pp. 75\u201397. IOS Press, (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-75","DOI":"10.3233\/978-1-58603-929-5-75"},{"key":"10168_CR25","doi-asserted-by":"publisher","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, volume 3709 of Lecture Notes in Computer Science, pp. 827\u2013831. Springer, (2005). https:\/\/doi.org\/10.1007\/11564751_73","DOI":"10.1007\/11564751_73"},{"key":"#cr-split#-10168_CR26.1","doi-asserted-by":"crossref","unstructured":"Tsejtin, G.S.: On the complexity of derivation in propositional calculus. Semin. Math. V. A. Steklov Math. Inst., Leningrad 8, 115-125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"#cr-split#-10168_CR26.2","unstructured":"translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 8, 234-259 (1968), 1968"},{"key":"10168_CR27","doi-asserted-by":"crossref","unstructured":"Valiant, L.G.: Graph-theoretic arguments in low-level complexity. In: International Symposium on Mathematical Foundations of Computer Science (1977)","DOI":"10.1007\/3-540-08353-7_135"},{"key":"10168_CR28","doi-asserted-by":"publisher","unstructured":"Valiant, L.G.: Graph-theoretic arguments in low-level complexity. In: Gruska, J. (ed.) Mathematical Foundations of Computer Science 1977, 6th Symposium, Tatranska Lomnica, Czechoslovakia, September 5\u20139, 1977, Proceedings, vol. 53 of Lecture Notes in Computer Science, pp. 162\u2013176. Springer, (1977). https:\/\/doi.org\/10.1007\/3-540-08353-7_135","DOI":"10.1007\/3-540-08353-7_135"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-024-10168-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-024-10168-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-024-10168-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,25]],"date-time":"2024-10-25T05:53:06Z","timestamp":1729835586000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-024-10168-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,26]]},"references-count":29,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["10168"],"URL":"https:\/\/doi.org\/10.1007\/s00224-024-10168-w","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-3171444\/v1","asserted-by":"object"}]},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,26]]},"assertion":[{"value":"29 February 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}