%% Theory of Computing
%% File: v009a014.bib
%% Publication date: May 27, 2013
%% Authors: Jakob Nordstrom and Johan Haastad
@string{acm      = "ACM Press"}
@string{ieee     = "IEEE Comp. Soc. Press"}
@string{springer = "Springer"}

@string{JACM="J. ACM"}
@string{SIAMJComput="SIAM J. Comput."}
@string{tcs      = "Theoret. Comput. Sci."}
@string{toc      = "Theory of Computing"}

@string{combinatorica    = "Combinatorica"}
@string{ccomplex = "Comput. Complexity"}
@string{discamath="Discr. Appl. Math."}
@string{eccc="Electron. Colloq. on Comput. Complexity (ECCC)"}
@string{InformandComput="Inform. and Comput."}
@string{ipl      = "Inform. Process. Lett."}
@string{JCombinTheorySerA="J. Combin. Theory Ser. A"}
@string{jcss="J. Comput. System Sci."}
@string{jsl = "J. Symbolic Logic"}
@string{RandomStructuresAlgorithms="Random Structures {\&} Algorithms"}

@string{stoc71="Proc. 3rd STOC"}
@string{stoc73="Proc. 5th STOC"}
@string{stoc74="Proc. 6th STOC"}
@string{stoc98="Proc. 30th STOC"}
@string{stoc99="Proc. 31st STOC"}
@string{stoc00="Proc. 32nd STOC"}
@string{stoc02="Proc. 34th STOC"}
@string{stoc06="Proc. 38th STOC"}
@string{stoc08="Proc. 40th STOC"}
@string{stoc12="Proc. 44th STOC"}

@string{focs83="Proc. 24th FOCS"}
@string{focs96="Proc. 37th FOCS"}
@string{focs97="Proc. 38th FOCS"}
@string{focs98="Proc. 39th FOCS"}
@string{focs99="Proc. 40th FOCS"}
@string{focs07="Proc. 48th FOCS"}
@string{focs08="Proc. 49th FOCS"}

@string{ccc=" IEEE Conf. on Computational Complexity"}
@string{ccc00="Proc. 15th" # ccc # " (CCC'00)"}
@string{ccc01="Proc. 16th" # ccc # " (CCC'01)"}
@string{ccc02="Proc. 17th" # ccc # " (CCC'02)"}
@string{ccc03="Proc. 18th" # ccc # " (CCC'03)"}

@string{icalp=" Internat. Colloq. on Automata, Languages and Programming"}
@string{icalp02= "Proc. 29th" # icalp # " (ICALP'02)"}

@string{stacs=" Symp. Theoretical Aspects of Comp. Sci."}
@string{stacs99= "Proc. 16th" # stacs  # " (STACS'99)"}

@inproceedings{jmnz12relatingproofcplx,
title = {Relating Proof Complexity Measures and Practical Hardness of {SAT}},
author = {Matti J{\"a}rvisalo and Arie Matsliah and Jakob Nordstr{\"o}m and Stanislav \v{Z}ivn\'{y}},
booktitle = {Proc. 18th Internat. Conf. on Principles and Practice of Constraint Programming (CP'12)},
publisher = springer,
year = {2012},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {316-331},
doi = {10.1007/978-3-642-33558-7\_25},
}
@article{bop07complexity,
title = {The complexity of resolution refinements},
author = {Joshua Buresh-Oppenheim and Toniann Pitassi},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/LICS.2003.1210053}{LICS'03}},
journal = jsl,
number = {4},
volume = {72},
year = {2007},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {1336-1352},
doi = {10.2178/jsl/1203350790},
}
%
@inproceedings{bop07complexity-conference,
title = {The Complexity of Resolution Refinements},
author = {Josh Buresh-Oppenheim and Toniann Pitassi},
booktitle = {18th IEEE Symp. on Logic in Computer Science (LICS'03)},
publisher = ieee,
year = {2003},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {138-147},
doi = {10.1109/LICS.2003.1210053},
}
@article{k80tightboundpebblespyramid,
title = {A Tight Bound for Black and White Pebbles on the Pyramid},
author = {Maria M. Klawe},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/SFCS.1983.3}{FOCS'83}},
journal = JACM,
number = {1},
volume = {32},
year = {1985},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {218-228},
doi = {10.1145/2455.214115},
}
%
@inproceedings{k80tightboundpebblespyramid-conference,
title = {A Tight Bound for Black and White Pebbles on the Pyramid},
author = {Maria M. Klawe},
crossref = {pfocs83},
year = {1983},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {410-419},
doi = {10.1109/SFCS.1983.3},
}


@techreport{gt78variationspebblegame,
title = {Variations of a Pebble Game on Graphs},
author = {John R. Gilbert and Robert Endre Tarjan},
number = {STAN-CS-78-661},
note = {\href{http://infolab.stanford.edu/TR/CS-TR-78-661.html}{InfoLab}},
year = {1978},
type = {Technical Report},
institution = {Stanford University},
eprint = {acm:892174},
}
%
@unpublished{nordstrom09pebblingsurveyfttcs,
title = {New Wine into Old Wineskins: A Survey of Some Pebbling Classics with Supplemental Results},
author = {Jakob Nordstr\"{o}m},
note = {Manuscript in preparation. To appear in \emph{Foundations and Trends in Theoretical Computer Science}. Current draft version available at \href{http://www.csc.kth.se/~jakobn/research/}{author's home page}},
year = {2013},
}

@article{razborov04resolutionlowerboundsforperfectmatching,
title = {Resolution Lower Bounds for Perfect Matching Principles},
author = {Alexander A. Razborov},
journal = jcss,
number = {1},
volume = {69},
year = {2004},
pages = {3--27},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/CCC.2002.1004336}{CCC'02}},
doi = {10.1016/j.jcss.2004.01.004},
} 
%
@inproceedings{razborov04resolutionlowerboundsforperfectmatching-conference,
title = {Resolution Lower Bounds for Perfect Matching Principles},
author = {Alexander A. Razborov},
booktitle = ccc02,
publisher = ieee,
year = {2002},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {29-38},
doi = {10.1109/CCC.2002.1004336},
}
%
@article{nordstrom10surveylmcs,
title = {Pebble Games, Proof Complexity and Time-Space Trade-offs},
author = {Jakob Nordstr\"{o}m},
journal = {Logical Methods in Computer Science},
note = {To appear. Available at \href{http://www.csc.kth.se/~jakobn/research/}{author's home page}},
year = {2013},
}

@article{abrw02spacecomplexity,
title = {Space Complexity in Propositional Calculus},
author = {Michael Alekhnovich and Eli {Ben-Sasson} and Alexander A. Razborov and Avi Wigderson},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/335305.335347}{STOC'00}},
journal = SIAMJComput,
number = {4},
volume = {31},
year = {2002},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {1184-1211},
doi = {10.1137/S0097539700366735},
}
%
@inproceedings{abrw02spacecomplexity-conference,
title = {Space complexity in propositional calculus},
author = {Michael Alekhnovich and Eli Ben-Sasson and Alexander A. Razborov and Avi Wigderson},
crossref = {pstoc00},
year = {2000},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {358-367},
doi = {10.1145/335305.335347},
}
%
@article{biw00near-optimalseparation,
title = {Near Optimal Separation Of Tree-Like And General Resolution},
author = {Eli {Ben-Sasson} and Russell Impagliazzo and Avi Wigderson},
journal = combinatorica,
number = {4},
volume = {24},
year = {2004},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {585-603},
doi = {10.1007/s00493-004-0036-5},
}
%
@article{segerlind07complexity,
title = {The Complexity of Propositional Proofs},
author = {Nathan Segerlind},
journal = {Bulletin of Symbolic Logic},
number = {4},
volume = {13},
year = {2007},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {417-481},
note = {\href{http://www.math.ucla.edu/~asl/bsl/1304-toc.htm}{Bulletin of Symbolic Logic}},
}


@inproceedings{bn11understandingspace,
title = {Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions},
author = {Eli Ben-Sasson and Jakob Nordstr{\"o}m},
booktitle = {Proc. 2nd Symp. Innovations in Computer Science (ICS'11)},
year = {2011},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {401-416},
note = {\href{http://conference.itcs.tsinghua.edu.cn/ICS2011/content/papers/3.html}{ICS'11}},
}
@article{bt88resolutionproofs,
title = {Resolution Proofs of Generalized Pigeonhole Principles},
author = {Samuel R. Buss and Gy\"{o}rgy Tur{\'a}n},
journal = tcs,
number = {3},
volume = {62},
year = {1988},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {311-317},
doi = {10.1016/0304-3975(88)90072-2},
}
@inproceedings{sbk03usingproblemstructure,
title = {Using Problem Structure for Efficient Clause Learning},
author = {Ashish Sabharwal and Paul Beame and Henry A. Kautz},
booktitle = {6th Internat. Conf. on Theory and Applications of Satisfiability Testing (SAT'03)},
year = {2004},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {242-256},
doi = {10.1007/978-3-540-24605-3\_19},
}


@article{egm04complexity,
title = {On the complexity of resolution with bounded conjunctions},
author = {Juan Luis Esteban and Nicola Galesi and Jochen Messner},
note = {Preliminary version in \href{http://dx.doi.org/10.1007/3-540-45465-9_20}{ICALP'02}},
journal = tcs,
number = {2-3},
volume = {321},
year = {2004},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {347-370},
doi = {10.1016/j.tcs.2004.04.004},
}
%
@inproceedings{egm04complexity-conference,
title = {On the Complexity of Resolution with Bounded Conjunctions},
author = {Juan Luis Esteban and Nicola Galesi and Jochen Messner},
booktitle = icalp02,
publisher = springer,
year = {2002},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {220-231},
doi = {10.1007/3-540-45465-9\_20},
}


@inproceedings{kullmann00matroid,
title = {An Application of Matroid Theory to the {SAT} Problem},
author = {Oliver Kullmann},
booktitle = ccc00,
publisher = ieee,
year = {2000},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {116-124},
doi = {10.1109/CCC.2000.856741},
}

@article{lt80spacecomplexitypebblegamestrees,
title = {The Space Complexity of Pebble Games on Trees},
author = {Thomas Lengauer and Robert Endre Tarjan},
journal = ipl,
number = {4-5},
volume = {10},
year = {1980},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {184-188},
doi = {10.1016/0020-0190(80)90136-2},
}


@article{r65machine-oriented,
title = {A Machine-Oriented Logic Based on the Resolution Principle},
author = {John Alan Robinson},
journal = JACM,
number = {1},
volume = {12},
year = {1965},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {23-41},
doi = {10.1145/321250.321253},
}
%
@misc{satcompetition,
title = {{T}he international {SAT} {C}ompetitions web page},
key = {SATcompetition},
note = {\url{http://www.satcompetition.org}},
}
%
@article{al86minimal,
title = {Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas},
author = {Ron Aharoni and Nathan Linial},
journal = JCombinTheorySerA,
number = {2},
volume = {43},
year = {1986},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {196-204},
doi = {10.1016/0097-3165(86)90060-9},
}


@inproceedings{cook71cookstheorem,
title = {The Complexity of Theorem-Proving Procedures},
author = {Stephen A. Cook},
crossref = {pstoc71},
year = {1971},
pages = {151-158},
doi = {10.1145/800157.805047},
}

@article{et01spacebounds,
title = {Space Bounds for Resolution},
author = {Juan Luis Esteban and Jacobo Tor{\'a}n},
note = {Preliminary versions in \href{http://dx.doi.org/10.1007/3-540-49116-3_52}{STACS'99} and \href{http://dx.doi.org/10.1007/3-540-48168-0_26}{CSL'99}},
journal = InformandComput,
number = {1},
volume = {171},
year = {2001},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {84-97},
doi = {10.1006/inco.2001.2921},
}
%
@inproceedings{et01spacebounds-stacs,
title = {Space Bounds for Resolution},
author = {Juan Luis Esteban and Jacobo Tor{\'a}n},
booktitle = stacs99,
publisher = springer,
year = {1999},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {551-560},
doi = {10.1007/3-540-49116-3\_52},
}
%
@inproceedings{et01spacebounds-csl,
  author    = {Jacobo Tor{\'a}n},
  title     = {Lower Bounds for Space in Resolution},
  booktitle = {13th Internat. Workshop on Computer Science Logic (CSL'99)},
  publisher = springer,
  year      = {1999},
  pages     = {362-373},
  doi       = {10.1007/3-540-48168-0\_26},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
%
@inproceedings{marques08practical,
title = {Practical Applications of {B}oolean Satisfiability},
author = {Jo{\~a}o P. {Marques-Silva}},
booktitle = {9th Internat. Workshop on Discrete Event Systems (WODES'08)},
year = {2008},
pages = {74-80},
doi = {10.1109/WODES.2008.4605925},
}

@article{cr79relative,
title = {The Relative Efficiency of Propositional Proof Systems},
author = {Stephen A. Cook and Robert A. Reckhow},
journal = jsl,
number = {1},
volume = {44},
year = {1979},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {36-50},
note = {\href{http://www.jstor.org/stable/2273702}{JSTOR}},
}
%
@article{c74observationtimestoragetradeoff,
title = {An Observation on Time-Storage Trade Off},
author = {Stephen A. Cook},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/800125.804032}{STOC'73}},
journal = jcss,
number = {3},
volume = {9},
year = {1974},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {308-316},
doi = {10.1016/S0022-0000(74)80046-2},
}
%
@inproceedings{c74observationtimestoragetradeoff-conference,
title = {An Observation on Time-Storage Trade Off},
author = {Stephen A. Cook},
crossref = {pstoc73},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {29-33},
doi = {10.1145/800125.804032},
}
%
@incollection{t68complexitytranslated,
title = {On the Complexity of Derivation in Propositional Calculus},
author = {Grigori Tseitin},
publisher = {Consultants Bureau, New~York-London},
booktitle = {Structures in Constructive Mathematics and mathematical Logic, Part II},
editor = {A. O. Silenko},
year = {1968},
pages = {115-125},
}

@article{dll62machineprogram,
title = {A machine program for theorem-proving},
author = {Martin Davis and George Logemann and Donald W. Loveland},
note = {},
journal = {Commun. ACM},
number = {7},
volume = {5},
year = {1962},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {394-397},
doi = {10.1145/368273.368557},
}


@article{bg03spacecomplexity,
title = {Space complexity of random formulae in resolution},
author = {Eli Ben-Sasson and Nicola Galesi},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/CCC.2001.933871}{CCC'01}},
journal = RandomStructuresAlgorithms,
number = {1},
volume = {23},
year = {2003},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {92-109},
doi = {10.1002/rsa.10089},
}
%
@inproceedings{bg03spacecomplexity-conference,
title = {Space Complexity of Random Formulae in Resolution},
author = {Eli Ben-Sasson and Nicola Galesi},
booktitle = ccc01,
publisher = ieee,
year = {2001},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {42-51},
doi = {10.1109/CCC.2001.933871},
}

@article{toran04space,
title = {Space and Width in Propositional Resolution},
author = {Jacobo Tor{\'a}n},
journal = {Bulletin of the EATCS},
volume = {83},
year = {2004},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {86-104},
note = {\href{http://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/toran/beatcs04.pdf}{Universit\"{a}t Ulm}},
}
@inproceedings{bs97usingcsp,
title = {Using {CSP} Look-Back Techniques to Solve Real-World {SAT} Instances},
author = {{Bayardo,~Jr.}, Roberto J. and Robert Schrag},
booktitle = {Proc. 14th Nat. Conf. on Artificial Intelligence (AAAI'97)},
year = {1997},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {203-208},
note = {\href{http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.1237}{CiteSeerX}},
eprint = {acm:1867406.1867438},
}


@inproceedings{nh08towardsoptimalseparationstoc,
title = {Towards an optimal separation of space and length in resolution},
author = {Jakob Nordstr{\"o}m and Johan H{\aa}stad},
crossref = {pstoc08},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {701-710},
doi = {10.1145/1374376.1374478},
}
@article{rm99separation,
title = {Separation of the Monotone {NC} Hierarchy},
author = {Ran Raz and Pierre McKenzie},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/SFCS.1997.646112}{FOCS'97}},
journal = combinatorica,
number = {3},
volume = {19},
year = {1999},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {403-435},
doi = {10.1007/s004930050062},
}
%
@inproceedings{rm99separation-conference,
title = {Separation of the Monotone {NC} Hierarchy},
author = {Ran Raz and Pierre McKenzie},
crossref = {pfocs97},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {234-243},
doi = {10.1109/SFCS.1997.646112},
}


@article{hp10pspacecompleteness,
title = {The {PSPACE}-Completeness of Black-White Pebbling},
author = {Philipp Hertel and Toniann Pitassi},
journal = SIAMJComput,
number = {6},
volume = {39},
year = {2010},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {2622-2682},
doi = {10.1137/080713513},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/FOCS.2007.22}{FOCS'07}},
}
%
@inproceedings{hp10pspacecompleteness-conference,
  author    = {Philipp Hertel and
               Toniann Pitassi},
  title     = {Exponential Time/Space Speedups for Resolution and the {PSPACE}-completeness
               of Black-White Pebbling},
  crossref  = {pfocs07},
  pages     = {137-149},
  doi       = {10.1109/FOCS.2007.22},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{ks07stateofsat,
title = {The state of {SAT}},
author = {Henry A. Kautz and Bart Selman},
journal = discamath,
number = {12},
volume = {155},
year = {2007},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {1514-1524},
doi = {10.1016/j.dam.2006.10.004},
}
%
@article{galil77resolution,
title = {On Resolution with Clauses of Bounded Size},
author = {Zvi Galil},
journal = SIAMJComput,
number = {3},
volume = {6},
year = {1977},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {444-459},
doi = {10.1137/0206031},
note = {Preliminary version found in \href{http://dx.doi.org/10.1145/800116.803755}{STOC'75}},
}
%
@inproceedings{galil77resolution-conference,
  author    = {Zvi Galil},
  title     = {On the Validity and Complexity of Bounded Resolution},
  crossref  = {pstoc75},
  pages     = {72-82},
  doi       = {10.1145/800116.803755},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{u87hardexamples,
title = {Hard examples for resolution},
author = {Alasdair Urquhart},
journal = JACM,
number = {1},
volume = {34},
year = {1987},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {209-219},
doi = {10.1145/7531.8928},
}

@article{nordstrom09narrowproofssicomp,
title = {Narrow Proofs May Be Spacious: Separating Space and Width in Resolution},
author = {Jakob Nordstr{\"o}m},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/1132516.1132590}{STOC'06}},
journal = SIAMJComput,
number = {1},
volume = {39},
year = {2009},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {59-121},
doi = {10.1137/060668250},
}
%
@inproceedings{nordstrom09narrowproofssicomp-conference,
title = {Narrow proofs may be spacious: separating space and width in resolution},
author = {Jakob Nordstr{\"o}m},
crossref = {pstoc06},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {507-516},
doi = {10.1145/1132516.1132590},
}
%
@article{bg01optimality,
title = {Optimality of size-width tradeoffs for resolution},
author = {Mar{\'i}a Luisa Bonet and Nicola Galesi},
journal = ccomplex,
number = {4},
volume = {10},
year = {2001},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {261-276},
doi = {10.1007/s000370100000},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/SFFCS.1999.814614}{FOCS'99}},
}
%
@inproceedings{bg01optimality-conference,
  author    = {Mar{\'i}a Luisa Bonet and
               Nicola Galesi},
  title     = {A Study of Proof Search Algorithms for Resolution and Polynomial Calculus},
  crossref  = {pfocs99},
  pages     = {422-432},
  doi       = {10.1109/SFFCS.1999.814614},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{h85intractability,
title = {The Intractability of Resolution},
author = {Armin Haken},
journal = tcs,
volume = {39},
year = {1985},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {297-308},
doi = {10.1016/0304-3975(85)90144-6},
}
%
@article{glt80pebblingproblemcomplete,
title = {The Pebbling Problem is Complete in Polynomial Space},
author = {John R. Gilbert and Thomas Lengauer and Robert Endre Tarjan},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/800135.804418}{STOC'79}},
journal = SIAMJComput,
number = {3},
volume = {9},
year = {1980},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {513-524},
doi = {10.1137/0209038},
}
%
@inproceedings{glt80pebblingproblemcomplete-conference,
title = {The Pebbling Problem is Complete in Polynomial Space},
author = {John R. Gilbert and Thomas Lengauer and Robert Endre Tarjan},
crossref = {pstoc79},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {237-248},
doi = {10.1145/800135.804418},
}


@article{dp60computingprocedure,
title = {A Computing Procedure for Quantification Theory},
author = {Martin Davis and Hilary Putnam},
journal = JACM,
number = {3},
volume = {7},
year = {1960},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {201-215},
doi = {10.1145/321033.321034},
}


@inproceedings{bbi12timespace,
title = {Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space},
author = {Paul Beame and Christopher Beck and Russell Impagliazzo},
crossref = {pstoc12},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {213-232},
doi = {10.1145/2213977.2213999},
}

@article{raz04resolution,
title = {Resolution lower bounds for the weak pigeonhole principle},
author = {Ran Raz},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/509907.509987}{STOC'02}},
journal = JACM,
number = {2},
volume = {51},
year = {2004},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {115-138},
doi = {10.1145/972639.972640},
}
%
@inproceedings{raz04resolution-conference,
title = {Resolution lower bounds for the weak pigeonhole principle},
author = {Ran Raz},
crossref = {pstoc02},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {553-562},
doi = {10.1145/509907.509987},
}
@article{bkps02efficiency,
title = {The Efficiency of Resolution and {D}avis--{P}utnam Procedures},
author = {Paul Beame and Richard M. Karp and Toniann Pitassi and Michael E. Saks},
journal = SIAMJComput,
number = {4},
volume = {31},
year = {2002},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {1048-1075},
doi = {10.1137/S0097539700369156},
note = {Preliminary versions in \href{http://dx.doi.org/10.1109/SFCS.1996.548486}{FOCS'96} and \href{http://dx.doi.org/10.1145/276698.276870}{STOC'98}}
}
%
@inproceedings{bkps02efficiency-stoc98,
  author    = {Paul Beame and
               Richard M. Karp and
               Toniann Pitassi and
               Michael E. Saks},
  title     = {On the Complexity of Unsatisfiability Proofs for Random
               $k$-{CNF} Formulas},
  crossref  = {pstoc98},
  pages     = {561-571},
  doi       = {10.1145/276698.276870},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
%
@inproceedings{bkps02efficiency-focs96,
  author    = {Paul Beame and
               Toniann Pitassi},
  title     = {Simplified and Improved Resolution Lower Bounds},
  crossref  = {pfocs96},
  pages     = {274-282},
  doi       = {10.1109/SFCS.1996.548486},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@phdthesis{alexhertel08thesis,
title = {Applications of Games to Propositional Proof Complexity},
author = {Alexander Hertel},
school = {University of Toronto},
note = {Available at \href{http://www.cs.utoronto.ca/~ahertel/}{author's home page}},
year = {2008},
eprint = {acm:1925663},
}

@article{bp98propositional,
title = {Propositional Proof Complexity: Past, Present and Future},
author = {Paul Beame and Toniann Pitassi},
journal = {Bulletin of the European Association for Theoretical Computer Science},
volume = {65},
year = {1998},
pages = {66-89},
note = {Available at \href{http://homes.cs.washington.edu/~beame/publications.html}{author's home page.} See also updated version at \href{http://eccc.hpi-web.de/report/1998/067/}{ECCC}},
}
%
@article{bp98propositional-eccc,
title = {Propositional Proof Complexity: Past, Present and Future},
author = {Paul Beame and Toniann Pitassi},
note = {\href{http://eccc.hpi-web.de/report/1998/067/}{ECCC}},
journal = eccc,
number = {67},
volume = {5},
year = {1998},
bibsource = {DBLP, http://dblp.uni-trier.de},
}


@article{et03combinatorialcharacterization,
title = {A combinatorial characterization of treelike resolution space},
author = {Juan Luis Esteban and Jacobo Tor{\'a}n},
journal = ipl,
number = {6},
volume = {87},
year = {2003},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {295-300},
doi = {10.1016/S0020-0190(03)00345-4},
}

@article{ajpu07exponentialseparation,
title = {An Exponential Separation between Regular and General Resolution},
author = {Michael Alekhnovich and Jan Johannsen and Toniann Pitassi and Alasdair Urquhart},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/509907.509974}{STOC'02}},
journal = toc,
number = {5},
volume = {3},
year = {2007},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {81-102},
doi = {10.4086/toc.2007.v003a005},
}
%
@inproceedings{ajpu07exponentialseparation-conference,
title = {An exponential separation between regular and general resolution},
author = {Michael Alekhnovich and Jan Johannsen and Toniann Pitassi and Alasdair Urquhart},
crossref = {pstoc02},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {448-456},
doi = {10.1145/509907.509974},
}
%
@inproceedings{ablm08measuring,
title = {Measuring the Hardness of {SAT} Instances},
author = {Carlos Ans{\'o}tegui and Mar{\'i}a Luisa Bonet and Jordi Levy and Felip Many{\`a}},
booktitle = {Proc. 23rd AAAI Conference on Artificial Intelligence (AAAI'08)},
publisher = {AAAI Press},
year = {2008},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {222-228},
eprint = {acm:1620032},
note = {\href{https://www.aaai.org/Papers/AAAI/2008/AAAI08-035.pdf}{AAAI}},
}
%
@article{cs76storage,
title = {Storage Requirements for Deterministic Polynomial Time Recognizable Languages},
author = {Stephen A. Cook and Ravi Sethi},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/800119.803882}{STOC'74}},
journal = jcss,
number = {1},
volume = {13},
year = {1976},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {25-37},
doi = {10.1016/S0022-0000(76)80048-7},
}
%
@inproceedings{cs76storage-conference,
title = {Storage Requirements for Deterministic / Polynomial Time Recognizable Languages},
author = {Stephen A. Cook and Ravi Sethi},
crossref = {pstoc74},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {33-39},
doi = {10.1145/800119.803882},
}
%
%
@article{ss96grasp,
title = {{GRASP}: A Search Algorithm for Propositional Satisfiability},
author = {Jo{\~a}o P. {Marques-Silva} and Karem A. Sakallah},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/ICCAD.1996.569607}{ICCAD'96}},
journal = {IEEE Trans. Computers},
number = {5},
volume = {48},
year = {1999},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {506-521},
doi = {10.1109/12.769433},
}
%
@inproceedings{ss96grasp-original,
title = {{GRASP}--a new search algorithm for satisfiability},
author = {Jo{\~{a}}o P. Marques-Silva and Karem A. Sakallah},
booktitle = {Internat. Conf. on Computer-Aided Design (ICCAD '96)},
publisher = ieee,
year = {1996},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {220-227},
doi = {10.1109/ICCAD.1996.569607},
}


@article{ad08combinatoricalcharacterization,
title = {A combinatorial characterization of resolution width},
author = {Albert Atserias and V\'{\i}ctor Dalmau},
journal = jcss,
number = {3},
volume = {74},
year = {2008},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {323-334},
doi = {10.1016/j.jcss.2007.06.025},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/CCC.2003.1214424}{CCC'03}},
}
%
@inproceedings{ad08combinatoricalcharacterization-conference,
title = {A combinatorial characterization of resolution width},
author = {Albert Atserias and V\'{\i}ctor Dalmau},
booktitle = ccc03,
publisher = ieee,
year = {2003},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {239-247},
doi = {10.1109/CCC.2003.1214424},
}

@article{bw01shortproofs,
title = {Short proofs are narrow - resolution made simple},
author = {Eli {Ben-Sasson} and Avi Wigderson},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/301250.301392}{STOC'99}},
journal = JACM,
number = {2},
volume = {48},
year = {2001},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {149-169},
doi = {10.1145/375827.375835},
}
%
@inproceedings{bw01shortproofs-conference,
title = {Short Proofs are Narrow - Resolution Made Simple},
author = {Eli {Ben-Sasson} and Avi Wigderson},
crossref = {pstoc99},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {517-526},
doi = {10.1145/301250.301392},
}


@article{razborov03resolutionlowerboundswfphp,
title = {Resolution lower bounds for the weak functional pigeonhole principle},
author = {Alexander A. Razborov},
journal = tcs,
number = {1},
volume = {303},
year = {2003},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {233-243},
doi = {10.1016/S0304-3975(02)00453-X},
}


@article{cs88manyhard,
title = {Many Hard Examples for Resolution},
author = {Va\v{s}ek Chv{\'a}tal and Endre Szemer{\'e}di},
journal = JACM,
number = {4},
volume = {35},
year = {1988},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {759-768},
doi = {10.1145/48014.48016},
}


@inproceedings{bn08shortproofs,
title = {Short Proofs May Be Spacious: An Optimal Separation of Space and Length in Resolution},
author = {Eli Ben-Sasson and Jakob Nordstr{\"o}m},
crossref = {pfocs08},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {709-718},
doi = {10.1109/FOCS.2008.42},
}
%
@article{begj00relativecomplexity,
title = {On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems},
author = {Mar{\'i}a Luisa Bonet and Juan Luis Esteban and Nicola Galesi and Jan Johannsen},
journal = SIAMJComput,
number = {5},
volume = {30},
year = {2000},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {1462-1484},
doi = {10.1137/S0097539799352474},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/SFCS.1998.743514}{FOCS'98}},
}
%
@inproceedings{begj00relativecomplexity-conference,
  author    = {Mar{\'i}a Luisa Bonet and
               Juan Luis Esteban and
               Nicola Galesi and
               Jan Johannsen},
  title     = {Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems},
  crossref  = {pfocs98},
  pages     = {638-647},
  doi       = {10.1109/SFCS.1998.743514},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
%
@phdthesis{b37canonical,
title = {Canonical Expressions in {B}oolean Algebra},
author = {Archie Blake},
school = {University of Chicago},
year = {1937},
}
%
@article{bet01minimallyunsatisfiable,
title = {Minimally Unsatisfiable {CNF} Formulas},
author = {Sven Baumer and Juan Luis Esteban and Jacobo Tor\'{a}n},
journal = {Bulletin of the European Association for Theoretical Computer Science},
volume = {74},
year = {2001},
pages = {190-192},
} 
%
@article{ben-sasson09sizespacetradeoffs,
title = {Size-Space Tradeoffs for Resolution},
author = {{Ben-Sasson}, Eli},
note = {Preliminary version in \href{http://dx.doi.org/10.1145/509907.509975}{STOC'02}},
journal = SIAMJComput,
number = {6},
volume = {38},
year = {2009},
pages = {2511-2525},
doi = {10.1137/080723880},
} 
%
@inproceedings{ben-sasson09sizespacetradeoffs-conference,
title = {Size space tradeoffs for resolution},
author = {Eli Ben-Sasson},
crossref = {pstoc02},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {457-464},
doi = {10.1145/509907.509975},
}
%
@article{hpv77timevsspace,
title = {On Time Versus Space},
author = {John E. Hopcroft and Wolfgang J. Paul and Leslie G. Valiant},
journal = JACM,
number = {2},
volume = {24},
year = {1977},
bibsource = {DBLP, http://dblp.uni-trier.de},
pages = {332-337},
doi = {10.1145/322003.322015},
note = {Preliminary version in \href{http://dx.doi.org/10.1109/SFCS.1975.23}{FOCS'75}},
}
%
@inproceedings{hpv77timevsspace-conference,
title = {On time versus space and related problems},
author = {John E. Hopcroft and Wolfgang J. Paul and Leslie G. Valiant},
crossref = {pfocs75},
pages = {57-64},
doi = {10.1109/SFCS.1975.23},
}

@incollection{b00proofcomplexity,
title = {Proof Complexity},
author = {Paul Beame},
publisher = {American Mathematical Society},
series = {IAS/Park City Mathematics Series},
booktitle = {Computational Complexity Theory},
volume = {10},
editor = {Steven Rudich and Avi Wigderson},
year = {2004},
pages = {199-246},
note = {Available at \href{http://www.cs.washington.edu/homes/beame/papers/lec.ps}{author's home page}},
} 
%
@techreport{p80pebbling,
title = {Pebbling},
author = {Nicholas Pippenger},
number = {RC8258},
note = {Appeared in Proceedings of the 5th IBM Symposium on Mathematical Foundations of Computer Science, Japan.},
year = {1980},
type = {Technical Report},
institution = {IBM Watson Research Center},
}

@proceedings{pstoc71,
booktitle = stoc71,
publisher = acm,
year = {1971}
}
@proceedings{pstoc73,
booktitle = stoc73,
publisher = acm,
year = {1973}
}
@proceedings{pstoc74,
booktitle = stoc74,
publisher = acm,
year = {1974}
}
@proceedings{pstoc98,
booktitle = stoc98,
publisher = acm,
year = {1998}
}
@proceedings{pstoc99,
booktitle = stoc99,
publisher = acm,
year = {1999}
}
@proceedings{pstoc00,
booktitle = stoc00,
publisher = acm,
year = {2000}
}
@proceedings{pstoc02,
booktitle = stoc02,
publisher = acm,
year = {2002}
}
@proceedings{pstoc06,
booktitle = stoc06,
publisher = acm,
year = {2006}
}
@proceedings{pstoc08,
booktitle = stoc08,
publisher = acm,
year = {2008}
}
@proceedings{pstoc12,
booktitle = stoc12,
publisher = acm,
year = {2012}
}

@proceedings{pfocs83,
booktitle = focs83,
publisher = ieee,
year = {1983}
}
@proceedings{pfocs96,
booktitle = focs96,
publisher = ieee,
year = {1996}
}
@proceedings{pfocs97,
booktitle = focs97,
publisher = ieee,
year = {1997}
}
@proceedings{pfocs98,
booktitle = focs98,
publisher = ieee,
year = {1998}
}
@proceedings{pfocs99,
booktitle = focs99,
publisher = ieee,
year = {1999}
}
@proceedings{pfocs07,
booktitle = focs07,
publisher = ieee,
year = {2007}
}
@proceedings{pfocs08,
booktitle = focs08,
publisher = ieee,
year = {2008}
}
