{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:14:04Z","timestamp":1759637644380},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319092836"},{"type":"electronic","value":"9783319092843"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_10","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T05:43:21Z","timestamp":1404279801000},"page":"121-137","source":"Crossref","is-referenced-by-count":6,"title":["Long Proofs of (Seemingly) Simple Formulas"],"prefix":"10.1007","author":[{"given":"Mladen","family":"Mik\u0161a","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Alekhnovich, M., Ben-Sasson, E., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM Journal on Computing\u00a031(4), 1184\u20131211 (2002), preliminary version appeared in STOC 2000","DOI":"10.1137\/S0097539700366735"},{"key":"10_CR2","unstructured":"Alekhnovich, M., Razborov, A.A.: Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics\u00a0242, 18\u201335 (2003), http:\/\/people.cs.uchicago.edu\/razborov\/files\/misha.pdf , Preliminary version appeared in FOCS 2001"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Atserias, A., Fichte, J.K., Thurley, M.: Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research\u00a040, 353\u2013373 (2011), preliminary version appeared in SAT 2009","DOI":"10.1613\/jair.3152"},{"key":"10_CR4","unstructured":"Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI 1997), pp. 203\u2013208 (July 1997)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Beck, C., Impagliazzo, R.: Strong ETH holds for regular resolution. In: Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 487\u2013494 (May 2013)","DOI":"10.1145\/2488608.2488669"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Wigderson, A.: Short proofs are narrow\u2014resolution made simple. Journal of the ACM 48\u00a048(2), 149\u2013169 (2001), preliminary version appeared in STOC 1999","DOI":"10.1145\/375827.375835"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation\u00a07, 59\u201364 (2010), system description","DOI":"10.3233\/SAT190075"},{"key":"10_CR8","series-title":"LNCS","first-page":"285","volume-title":"SAT 2014","author":"A. Biere","year":"2014","unstructured":"Biere, A., Le Berre, D., Lonca, E., Manthey, N.: Detecting cardinality constraints in CNF. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol.\u00a08561, pp. 285\u2013301. Springer, Heidelberg (2014)"},{"key":"10_CR9","unstructured":"Blake, A.: Canonical Expressions in Boolean Algebra. Ph.D. thesis, University of Chicago (1937)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Bondy, J.A., Murty, U.S.R.: Graph Theory. Springer (2008)","DOI":"10.1007\/978-1-84628-970-5"},{"issue":"4","key":"10_CR11","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1145\/48014.48016","volume":"35","author":"V. Chv\u00e1tal","year":"1988","unstructured":"Chv\u00e1tal, V., Szemer\u00e9di, E.: Many hard examples for resolution. Journal of the ACM\u00a035(4), 759\u2013768 (1988)","journal-title":"Journal of the ACM"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC 1996), pp. 174\u2013183 (May 1996)","DOI":"10.1145\/237814.237860"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W. Cook","year":"1987","unstructured":"Cook, W., Coullard, C.R., Tur\u00e1n, G.: On the complexity of cutting-plane proofs. Discrete Applied Mathematics\u00a018(1), 25\u201338 (1987)","journal-title":"Discrete Applied Mathematics"},{"key":"10_CR14","unstructured":"The Glucose SAT solver, http:\/\/www.labri.fr\/perso\/lsimon\/glucose\/ ."},{"issue":"2-3","key":"10_CR15","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theoretical Computer Science\u00a039(2-3), 297\u2013308 (1985)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10_CR16","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1090\/S0273-0979-06-01126-8","volume":"43","author":"S. Hoory","year":"2006","unstructured":"Hoory, S., Linial, N., Wigderson, A.: Expander graphs and their applications. Bulletin of the American Mathematical Society\u00a043(4), 439\u2013561 (2006)","journal-title":"Bulletin of the American Mathematical Society"},{"issue":"2","key":"10_CR17","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s000370050024","volume":"8","author":"R. Impagliazzo","year":"1999","unstructured":"Impagliazzo, R., Pudl\u00e1k, P., Sgall, J.: Lower bounds for the polynomial calculus and the Gr\u00f6bner basis algorithm. Computational Complexity\u00a08(2), 127\u2013144 (1999)","journal-title":"Computational Complexity"},{"key":"10_CR18","unstructured":"Lingeling and Plingeling, http:\/\/fmv.jku.at\/lingeling\/"},{"key":"10_CR19","unstructured":"March, http:\/\/www.st.ewi.tudelft.nl\/~marijn\/sat\/march_dl.php"},{"issue":"1-4","key":"10_CR20","doi-asserted-by":"crossref","first-page":"221","DOI":"10.3233\/SAT190024","volume":"2","author":"K. Markstr\u00f6m","year":"2006","unstructured":"Markstr\u00f6m, K.: Locality and hard SAT-instances. Journal on Satisfiability, Boolean Modeling and Computation\u00a02(1-4), 221\u2013227 (2006)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999), preliminary version appeared in ICCAD 1996","DOI":"10.1109\/12.769433"},{"key":"10_CR22","unstructured":"The MiniSat page, http:\/\/minisat.se\/"},{"key":"10_CR23","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), pp. 530\u2013535 (June 2001)","DOI":"10.1145\/378239.379017"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Nordstr\u00f6m, J.: Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science\u00a09, 15:1\u201315:63 (2013)","DOI":"10.2168\/LMCS-9(3:15)2013"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: On the power of clause-learning SAT solvers as resolution engines. Artificial Intelligence\u00a0175, 512\u2013525 (2011), preliminary version appeared in CP 2009","DOI":"10.1016\/j.artint.2010.10.002"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Spence, I.: sgen1: A generator of small but difficult satisfiability benchmarks. Journal of Experimental Algorithmics\u00a015, 1.2:1.1\u20131.2:1.15 (2010)","DOI":"10.1145\/1671970.1671972"},{"issue":"1","key":"10_CR27","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A. Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. Journal of the ACM\u00a034(1), 209\u2013219 (1987)","journal-title":"Journal of the ACM"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-14186-7_37","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A. Gelder Van","year":"2010","unstructured":"Van Gelder, A., Spence, I.: Zero-one designs produce small hard SAT instances. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 388\u2013397. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,21]],"date-time":"2020-08-21T18:01:21Z","timestamp":1598032881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}