{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,24]],"date-time":"2026-01-24T23:44:23Z","timestamp":1769298263810,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141850","type":"print"},{"value":"9783642141867","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-14186-7_8","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:20:37Z","timestamp":1278627637000},"page":"71-84","source":"Crossref","is-referenced-by-count":13,"title":["Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT"],"prefix":"10.1007","author":[{"given":"Carsten","family":"Fuhs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schneider-Kamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02777-2_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"R. As\u00edn","year":"2009","unstructured":"As\u00edn, R., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Cardinality networks and their applications. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 167\u2013180. Springer, Heidelberg (2009)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-85238-4_13","volume-title":"Mathematical Foundations of Computer Science 2008","author":"J. Boyar","year":"2008","unstructured":"Boyar, J., Matthews, P., Peralta, R.: On the shortest linear straight-line program for computing linear forms. In: Ochma\u0144ski, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol.\u00a05162, pp. 168\u2013179. Springer, Heidelberg (2008)"},{"key":"8_CR3","unstructured":"Boyar, J., Peralta, R.: A new technique for combinational circuit optimization and a new circuit for the S-Box for AES. In: Patent Application Number 61089998 filed with the U.S. Patent and Trademark Office (2009)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-642-13193-6_16","volume-title":"Proc. International Symposium on Experimental Algorithms (SEA 2010)","author":"J. Boyar","year":"2010","unstructured":"Boyar, J., Peralta, R.: A new combinational logic minimization technique with applications to cryptology. In: Festa, P. (ed.) SEA 2010. LNCS, vol.\u00a06049, pp. 178\u2013189. Springer, Heidelberg (2010)"},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"193","DOI":"10.3233\/SAT190056","volume":"5","author":"M. Codish","year":"2008","unstructured":"Codish, M., Lagoon, V., Stuckey, P.: Solving partial order constraints for LPO termination. Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a05, 193\u2013215 (2008)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation (JSAT)"},{"issue":"1-4","key":"8_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190014","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating pseudo-boolean constraints into SAT. Journal on Satisfiability, Boolean Modelling and Computation (JSAT)\u00a02(1-4), 1\u201326 (2006)","journal-title":"Journal on Satisfiability, Boolean Modelling and Computation (JSAT)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Thiemann, R., Schneider-Kamp, P., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"8_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"8_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/11814771_40","volume-title":"Automated Reasoning","author":"O. Grinchtein","year":"2006","unstructured":"Grinchtein, O., Leucker, M., Piterman, N.: Inferring network invariants automatically. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 483\u2013497. Springer, Heidelberg (2006)"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"H. Hong","year":"1998","unstructured":"Hong, H., Jaku\u0161, D.: Testing positiveness of polynomials. Journal of Automated Reasoning (JAR)\u00a021(1), 23\u201338 (1998)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02777-2_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A. Kojevnikov","year":"2009","unstructured":"Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: Finding efficient circuits using SAT-solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 32\u201344. Springer, Heidelberg (2009)"},{"key":"8_CR12","unstructured":"Le Berre, D., Parrain, A.: SAT4J, http:\/\/www.sat4j.org"},{"key":"8_CR13","unstructured":"Federal Information Processing\u00a0Standard 197. The advanced encryption standard. Technical report, National Institute of Standards and Technology (2001)"},{"key":"#cr-split#-8_CR14.1","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1968);","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"#cr-split#-8_CR14.2","unstructured":"Reprinted in Automation of Reasoning 2, 466\u2013483 (1983)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T19:42:16Z","timestamp":1591472536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}