{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T03:08:00Z","timestamp":1769742480786,"version":"3.49.0"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66263-3_30","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"464-473","source":"Crossref","is-referenced-by-count":19,"title":["CNFgen: A Generator of Crafted Benchmarks"],"prefix":"10.1007","author":[{"given":"Massimo","family":"Lauria","sequence":"first","affiliation":[]},{"given":"Jan","family":"Elffers","sequence":"additional","affiliation":[]},{"given":"Jakob","family":"Nordstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Vinyals","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"issue":"4","key":"30_CR1","doi-asserted-by":"crossref","first-page":"1184","DOI":"10.1137\/S0097539700366735","volume":"31","author":"M Alekhnovich","year":"2002","unstructured":"Alekhnovich, M., Ben-Sasson, E., Alexander, A., Razborov, A.A., Wigderson, A.: Space complexity in propositional calculus. SIAM J. Comput. 31(4), 1184\u20131211 (2002). Preliminary version in STOC \u201900","journal-title":"SIAM J. Comput."},{"issue":"5","key":"30_CR2","doi-asserted-by":"crossref","first-page":"81","DOI":"10.4086\/toc.2007.v003a005","volume":"3","author":"M Alekhnovich","year":"2007","unstructured":"Alekhnovich, M., Johannsen, J., Pitassi, T., Urquhart, A.: An exponential separation between regular and general resolution. Theor. Comput. 3(5), 81\u2013102 (2007). Preliminary version in STOC \u201902","journal-title":"Theor. Comput."},{"key":"30_CR3","unstructured":"Alekhnovich, M., Alexander, A. Razborov, A.A.: Lower bounds for polynomial calculus: Non-binomial case. In: Proceedings of the Steklov Institute of Mathematics, 242, 18\u201335 (2003). http:\/\/people.cs.uchicago.edu\/~razborov\/files\/misha.pdf . Preliminary version in FOCS \u201901"},{"key":"30_CR4","unstructured":"Balyo, T., Marijn, J., Heule, H., J\u00e4rvisalo, M.: Proceedings of SAT competition 2016: Solver and benchmark descriptions. Technical report B-2016-1, University of Helsinki (2016). http:\/\/hdl.handle.net\/10138\/164630"},{"key":"30_CR5","unstructured":"Roberto, J., Bayardo, Jr., 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 (1997)"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Beame, P., Beck, C., Impagliazzo, R.: Time-space tradeoffs in resolution: Superpolynomial lower bounds for superlinear space. In: Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pp. 213\u2013232 (2012)","DOI":"10.1145\/2213977.2213999"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Beck, C., Nordstr\u00f6m, J., Tang, B.: Some trade-off results for polynomial calculus. In: Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC 2013), pp. 813\u2013822 (2013)","DOI":"10.1145\/2488608.2488711"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Short proofs may be spacious: An optimal separation of space and length in resolution. In: Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2008), pp. 709\u2013718 (2008)","DOI":"10.1109\/FOCS.2008.42"},{"key":"30_CR9","unstructured":"Ben-Sasson, E., Nordstr\u00f6m, J.: Understanding space in proof complexity: Separations and trade-offs via substitutions. In: Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS 2011), pp. 401\u2013416 (2011)"},{"issue":"3","key":"30_CR10","doi-asserted-by":"crossref","first-page":"20:1","DOI":"10.1145\/2499937.2499941","volume":"14","author":"O Beyersdorff","year":"2013","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M.: Parameterized complexity of DPLL search procedures. ACM Trans. Comput. Logic 14(3), 20:1\u201320:21 (2013). Preliminary version in SAT \u201911","journal-title":"ACM Trans. Comput. Logic"},{"key":"30_CR11","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2355580.2355582","volume":"4","author":"O Beyersdorff","year":"2012","unstructured":"Beyersdorff, O., Galesi, N., Lauria, M., Razborov, A.A.: Parameterized bounded-depth Frege is not optimal. ACM Trans. Comput. Theor. 4, 7:1\u20137:16 (2012). Preliminary version in ICALP \u201911","journal-title":"ACM Trans. Comput. Theor."},{"key":"30_CR12","unstructured":"Blake, A.: Canonical expressions in boolean algebra. PhD thesis, University of Chicago (1937)"},{"issue":"4","key":"30_CR13","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s000370100000","volume":"10","author":"ML Bonet","year":"2001","unstructured":"Bonet, M.L., Galesi, N.: Optimality of size-width tradeoffs for resolution. Comput. Complex. 10(4), 261\u2013276 (2001). Preliminary version in FOCS \u201999","journal-title":"Comput. Complex."},{"issue":"9","key":"30_CR14","doi-asserted-by":"crossref","first-page":"1326","DOI":"10.1016\/j.jsc.2008.02.017","volume":"44","author":"M Brickenstein","year":"2009","unstructured":"Brickenstein, M., Dreyer, A.: PolyBoRi: A framework for Gr\u00f6bner-basis computations with Boolean polynomials. J. Symb. Comput. 44(9), 1326\u20131345 (2009)","journal-title":"J. Symb. Comput."},{"issue":"8","key":"30_CR15","doi-asserted-by":"crossref","first-page":"1612","DOI":"10.1016\/j.jpaa.2008.11.043","volume":"213","author":"M Brickenstein","year":"2009","unstructured":"Brickenstein, M., Dreyer, A., Greuel, G.-M., Wedler, M., Wienand, O.: New developments in the theory of Gr\u00f6bner bases and applications to formal verification. J. Pure Appl. Algebr. 213(8), 1612\u20131635 (2009)","journal-title":"J. Pure Appl. Algebr."},{"issue":"2","key":"30_CR16","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1006\/jcss.2000.1726","volume":"62","author":"SR Buss","year":"2001","unstructured":"Buss, S.R., Grigoriev, D., Impagliazzo, R., Pitassi, T.: Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci. 62(2), 267\u2013289 (2001). Preliminary version in CCC \u201999","journal-title":"J. Comput. Syst. Sci."},{"key":"30_CR17","first-page":"10:16","volume":"10","author":"SR Buss","year":"2014","unstructured":"Buss, S.R., Ko\u0142odziejczyk, L.: Small stone in pool. Logic. Method. Comput. Sci. 10, 10:16\u201316:22 (2014)","journal-title":"Logic. Method. Comput. Sci."},{"issue":"3","key":"30_CR18","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1109\/TCAD.2004.842808","volume":"24","author":"D Chai","year":"2005","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(3), 305\u2013317 (2005). Preliminary version in DAC \u201903","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"4","key":"30_CR19","doi-asserted-by":"crossref","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. J. ACM 35(4), 759\u2013768 (1988)","journal-title":"J. ACM"},{"key":"30_CR20","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 (1996)","DOI":"10.1145\/237814.237860"},{"key":"30_CR21","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pp. 151\u2013158 (1971)","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"30_CR22","doi-asserted-by":"crossref","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.: The relative efficiency of propositional proof systems. J. Symbol. Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symbol. Logic"},{"issue":"1","key":"30_CR23","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0166-218X(87)90039-4","volume":"18","author":"W Cook","year":"1987","unstructured":"Cook, W.: Collette Rene Coullard, and Gy\u00f6rgy Tur\u00e1n. On the complexity of cutting-plane proofs. Discr. Appl. Math. 18(1), 25\u201338 (1987)","journal-title":"Discr. Appl. Math."},{"key":"30_CR24","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1613\/jair.1656","volume":"23","author":"HE Dixon","year":"2005","unstructured":"Dixon, H.E., Ginsberg, M.L., Hofer, D.K., Luks, E.M., Parkes, A.J.: Generalizing Boolean satisfiability III: Implementation. J. Artif. Intell. Res. 23, 441\u2013531 (2005)","journal-title":"J. Artif. Intell. Res."},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"Elffers, J., Gir\u00e1ldez-Cr\u00fa, J., Nordstr\u00f6m, J., Vinyals, M.: Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers (2017, Submitted)","DOI":"10.1007\/978-3-319-94144-8_5"},{"key":"30_CR26","unstructured":"Elffers, J., Nordstr\u00f6m, J., Simon, L., Sakallah, K.A.: Seeking practical CDCL insights from theoretical SAT benchmarks. In: Presentation at the Pragmatics of SAT 2016 workshop (2016). http:\/\/www.csc.kth.se\/~jakobn\/research\/TalkPoS16.pdf"},{"key":"30_CR27","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.1145\/1838552.1838556","volume":"12","author":"N Galesi","year":"2010","unstructured":"Galesi, N., Lauria, M.: Optimality of size-degree trade-offs for polynomial calculus. ACM Trans. Comput. Logic 12, 4:1\u20134:22 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"key":"30_CR28","doi-asserted-by":"crossref","unstructured":"Hagberg, A.A., Schult, D., Swart, P.S.: Exploring network structure, dynamics, and function using NetworkX. In: Proceedings of the 7th Python in Science Conference (SciPy2008), Pasadena, CA USA, pp. 11\u201315 (2008)","DOI":"10.25080\/TCWV9851"},{"issue":"2\u20133","key":"30_CR29","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 39(2\u20133), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/11527695_12","volume-title":"Theory and Applications of Satisfiability Testing","author":"M Heule","year":"2005","unstructured":"Heule, M., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 145\u2013156. Springer, Heidelberg (2005). doi: 10.1007\/11527695_12"},{"key":"30_CR31","unstructured":"Himsolt, M.: GML: A portable graph file format. Technical report, Universit\u00e4t of Passau (1996)"},{"key":"30_CR32","doi-asserted-by":"crossref","unstructured":"Huynh, T., Nordstr\u00f6m, J.: On the virtue of succinct proofs: Amplifying communication complexity hardness to time-space trade-offs in proof complexity (Extended abstract). In: Proceedings of the 44th Annual ACM Symposium on Theory of Computing (STOC 2012), pp. 233\u2013248 (2012)","DOI":"10.1145\/2213977.2214000"},{"issue":"2","key":"30_CR33","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1006\/jcss.2000.1727","volume":"62","author":"R Impagliazzo","year":"2001","unstructured":"Impagliazzo, R., Paturi, R.: On the complexity of $$k$$ -SAT. J. Comput. Syst. Sci. 62(2), 367\u2013375 (2001). Preliminary version in CCC \u201999","journal-title":"J. Comput. Syst. Sci."},{"key":"30_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-33558-7_25","volume-title":"Principles and Practice of Constraint Programming","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Matsliah, A., Nordstr\u00f6m, J., \u017divn\u00fd, S.: Relating proof complexity measures and practical hardness of SAT. In: Milano, M. (ed.) CP 2012. LNCS, pp. 316\u2013331. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33558-7_25"},{"key":"30_CR35","first-page":"59","volume":"7","author":"D Berre Le","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. J. Satisf. Boolean Model. Comput. 7, 59\u201364 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"1\u20134","key":"30_CR36","first-page":"221","volume":"2","author":"K Markstr\u00f6m","year":"2006","unstructured":"Markstr\u00f6m, K.: Locality and hard SAT-instances. J. Satisf. Boolean Model. Comput. 2(1\u20134), 221\u2013227 (2006)","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"5","key":"30_CR37","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999). Preliminary version in ICCAD \u201996","journal-title":"IEEE Trans. Comput."},{"key":"30_CR38","unstructured":"Massey, B.: DIMACS graph format (2001). http:\/\/prolland.free.fr\/works\/research\/dsat\/dimacs.html . Accessed 11 Feb 2016"},{"key":"30_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-09284-3_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"M Mik\u0161a","year":"2014","unstructured":"Mik\u0161a, M., Nordstr\u00f6m, J.: Long proofs of (seemingly) simple formulas. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 121\u2013137. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_10"},{"key":"30_CR40","unstructured":"Mik\u0161a, M., Nordstr\u00f6m, J.: A generalized method for proving polynomial calculus degree lower bounds. In: Proceedings of the 30th Annual Computational Complexity Conference (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol. 33, pp. 467\u2013487 (2015)"},{"key":"30_CR41","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Chaff, M.S.: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"30_CR42","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2815493.2815497","volume":"2","author":"J Nordstr\u00f6m","year":"2015","unstructured":"Nordstr\u00f6m, J.: On the interplay between proof complexity and SAT solving. ACM SIGLOG News 2(3), 19\u201344 (2015)","journal-title":"ACM SIGLOG News"},{"key":"30_CR43","unstructured":"Pseudo-Boolean competition (2016). http:\/\/www.cril.univ-artois.fr\/PB16\/"},{"issue":"1","key":"30_CR44","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.jcss.2004.01.004","volume":"69","author":"AA Razborov","year":"2004","unstructured":"Razborov, A.A.: Resolution lower bounds for perfect matching principles. J. Comput. Syst. Sci. 69(1), 3\u201327 (2004). Preliminary version in CCC \u201902","journal-title":"J. Comput. Syst. Sci."},{"key":"30_CR45","doi-asserted-by":"crossref","first-page":"16:1","DOI":"10.1145\/2858790","volume":"63","author":"AA Razborov","year":"2016","unstructured":"Razborov, A.A.: A new kind of tradeoffs in propositional proof complexity. J. ACM 63, 16:1\u201316:14 (2016)","journal-title":"J. ACM"},{"key":"30_CR46","unstructured":"AT and T Research: Dot Language. http:\/\/www.graphviz.org\/content\/dot-language . Accessed 11 Feb 2016"},{"issue":"1\u20134","key":"30_CR47","first-page":"165","volume":"2","author":"HM Sheini","year":"2006","unstructured":"Sheini, H.M., Sakallah, K.A.: Pueblo: a hybrid pseudo-Boolean SAT solver. J. Satisf. Boolean Model. Comput. 2(1\u20134), 165\u2013189 (2006). Preliminary version in DATE \u201905","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"30_CR48","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). doi: 10.1007\/978-3-642-02777-2_24"},{"issue":"3","key":"30_CR49","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/s002360050044","volume":"33","author":"G St\u00e5lmarck","year":"1996","unstructured":"St\u00e5lmarck, G.: Short resolution proofs for a sequence of tricky formulas. Acta Inform. 33(3), 277\u2013280 (1996)","journal-title":"Acta Inform."},{"issue":"1","key":"30_CR50","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (1987)","journal-title":"J. ACM"},{"key":"30_CR51","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","year":"2010","unstructured":"Gelder, A., Spence, I.: Zero-one designs produce small hard SAT instances. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 388\u2013397. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14186-7_37"},{"key":"30_CR52","doi-asserted-by":"crossref","unstructured":"Vinyals, M., Elffers, J., Gir\u00e1ldez-Cr\u00fa, J., Gocht, S., Nordstr\u00f6m, J.: In between resolution and cutting planes: A study of proof systems for pseudo-Boolean SAT solving (2017, Submitted)","DOI":"10.1007\/978-3-319-94144-8_18"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T20:59:56Z","timestamp":1750798796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}