@STRING{siam = "SIAM Journal of Computing"}
@STRING{comb = "Combinatorica"}
@STRING{mst = "Mathematical Systems Theory"}

@INPROCEEDINGS{bhp,
 	AUTHOR = {Fahiem Bacchus and Philipp Hertel and Toniann Pitassi},
	TITLE = {The Complexity of Resolution with Caching},
	NOTE = {Unpublished manuscript},
	Year =  {2006}
}

@INPROCEEDINGS{beapit96b,
   AUTHOR = {Paul Beame and Toniann Pitassi},
   TITLE = {Simplified and Improved Resolution Lower Bounds},
   YEAR = {1996},
   BOOKTITLE = {Proc.\ 37th FOCS},
   publisher = {IEEE Comp. Soc. Press},
pages="274--282",
eprint="focs:10.1109/SFCS.1996.548486"
}

@UNPUBLISHED{benimpwig00,
   AUTHOR = {Eli Ben-Sasson and Russell Impagliazzo and Avi Wigderson},
   TITLE = {Near-Optimal Separation of Tree-like and General Resolution},
   NOTE = {ECCC TR00-005},
   YEAR = {2000},
eprint="eccc:TR00-005"
}


@INPROCEEDINGS{bg99,
   AUTHOR = {M. Bonet and N. Galesi},
   TITLE = {A Study of Proof Search Algorithms for Resolution and Polynomial Calculus},
   YEAR = {1999},
   PAGES = {422--432},
   BOOKTITLE = {Proc.\ 40th FOCS},
   publisher = {IEEE Comp. Soc. Press},
eprint="focs:10.1109/SFFCS.1999.814614"
}


@ARTICLE{bonestgaljoh00,
   AUTHOR = {Maria Luisa Bonet and Juan Luis Esteban and Nicola Galesi and Jan Johannsen},
   TITLE = {On the Relative Complexity of Resolution Restrictions and Cutting Planes Proof Systems},
   JOURNAL = siam,
   VOLUME = {30},
   YEAR = {2000},
   PAGES = {1462--1484},
eprint="sicomp:10.1137/S0097539799352474"
}

@INPROCEEDINGS{burcleimppit00,
   AUTHOR = {Buresh-Oppenheim, Joshua and Clegg, Matthew and Impagliazzo, Russell and Pitassi, Toniann},
   TITLE = {Homogenization and the Polynomial Calculus},
   BOOKTITLE = {Proc. 27th International Colloquium on Automata, Languages and Programming},
   PAGES = {926--937},
   YEAR = {2000},
   PUBLISHER = {Springer},
eprint="icalp:fvxybba423y153b8"
}

@ARTICLE{cpt77,
   AUTHOR = {Celoni, James and Paul, Wolfgang and Tarjan, Robert},
   TITLE = {Space Bounds for a Game on Graphs},
   JOURNAL = mst,
   VOLUME = {10},
   YEAR = {1977},
   PAGES = {239--251},
eprint="springer:u32u2r202jv33611"
}

@ARTICLE{cook76,
	AUTHOR   = {Stephen A.~Cook},
	TITLE =    {A short proof of the pigeon hole principle
			using extended resolution},
	YEAR = {1976},
	JOURNAL = {SIGACT News},
	VOLUME = {8},
number=4,
	PAGES = {28--32},
eprint="sigact:10.1145/1008335.1008338"
}

@ARTICLE{cr79,
   AUTHOR = {Stephen A.~Cook and Robert A.~Reckhow},
   TITLE = {The relative efficiency of propositional proof systems},
   JOURNAL = {Journal of Symbolic Logic} ,
   VOLUME = 6,
   PAGES = "169--184",
   YEAR = 1979
}

@article{dll62,
	author = "Martin Davis  and George Logemann and Donald Loveland",
	title = "A Machine Program for Theorem Proving",
	journal = "Communications of the Association for Computing Machinery",
	volume = 5,
	pages = "394--397",
	year = 1962,
eprint="acm:10.1145/368273.368557"
	}


@ARTICLE{beame-kautz,
   AUTHOR = "Paul Beame and Henry Kautz and Ashish Sabharwal",
   TITLE = "Towards understanding and harnessing the potential of clause learning",
   JOURNAL = {Journal of Artifical Intelligence Research},
   VOLUME = 22,
   YEAR = 2004,
pages="319--351",
url="http://www.jair.org/papers/paper1410.html"
}


@ARTICLE{g92,
   AUTHOR = {Andreas Goerdt},
   TITLE = {Davis-{P}utnam Resolution versus Unrestricted Resolution},
   JOURNAL= {Annals of Mathematics and Artificial Intelligence} ,
   VOLUME = 6,
   PAGES = "169--184",
   YEAR = 1992,
eprint="springer:k008110v05867897"
}

@ARTICLE{goe93,
   AUTHOR = {Andreas Goerdt},
   TITLE = {Regular Resolution versus Unrestricted Resolution},
   JOURNAL = siam,
   PAGES = {661--683},
   VOLUME = {22},
   YEAR = {1993},
eprint="sicomp:10.1137/0222044"
}

@article{hak85,	
	author = "Armin Haken",
	title = "The intractability of resolution",	
	journal = "Theoretical Computer Science",
	volume = 39,
	year = 1985,
	pages = "297--308",
eprint="tcs:10.1016/0304-3975(85)90144-6"}

  
@ARTICLE{huang87,
   AUTHOR = {Wenqi Huang and Xiangdong Yu},
   TITLE = {A {DNF} without regular shortest consensus path},
   JOURNAL = "SIAM Journal on Computing",
   VOLUME = {16},
   YEAR = {1987},
   PAGES = {836--840},
eprint="sicomp:10.1137/0216054"
   }
	
@book{kraj95,
	author = "Jan {Kraj\'{\i}\v{c}ek}",
	title = "Bounded Arithmetic, Propositional Logic and Complexity Theory",
	publisher = "Cambridge University Press",
	year = 1995}	

@ARTICLE{krish85,
   AUTHOR = "Balakrishnan Krishnamurthy",
   TITLE = "Short proofs for tricky formulas",
   JOURNAL = "Acta Informatica",
   VOLUME = 22,
   PAGES = "253--274", 
   YEAR = 1985,
eprint="actainf:mp65776636126242"
}

@mastersthesis{nadel,
   AUTHOR = {Alexander Nadel},
   TITLE = {Backtrack search algorithms for propositional logic satisfiability: Review and innovations},
   SCHOOL = {Hebrew University},
   YEAR = 2002
}

@INPROCEEDINGS{minisat,
   AUTHOR = {Niklas Een and Niklas {S\"{o}rensson}},
   TITLE = {An extensible {SAT}-solver},
   BOOKTITLE = {Proc.\ 6th International Conference on Theory and Applications of Satisfiability Testing},
pages="502--518",
   YEAR = 2003,
   publisher = {Springer},
eprint="springer:x9uavq4vpvqntt23"
}

@INPROCEEDINGS{zchaff,
   AUTHOR = {Matthew Moskewicz and Conor Madigan and Ying Zhao and Lintao Zhang and Sharad Malik},
   TITLE = {Chaff: Engineering an Efficient {SAT} Solver},
   BOOKTITLE = {Proc.\ 38th Design Automation Conference},
   YEAR = 2001,
pages="530--535",
publisher = {ACM Press},
eprint="acm:10.1145/378239.379017"
}
  
@ARTICLE{razmck99,
   AUTHOR = {Ran Raz and Pierre McKenzie},
   TITLE = {Separation of the Monotone {NC} Hierarchy},
   JOURNAL = comb,
   VOLUME = {19},
   YEAR = {1999},
   PAGES = {403--435},
   NOTE = {Preliminary Version in: {\em Proc.\ 38th FOCS}, 1997},
eprint="springer:h4prxbwxpn1c8xqh"
}

@article{stalmarck96,
	author = "Gunnar {St\r{a}lmarck}",
	title = "Short resolution proofs for a sequence of tricky formulas",
	journal = "Acta Informatica",
	volume = 33,
	pages = "277--280",
	year = 1996,
eprint="actainf:lhrhe2glkmgflbu1"}

@book{sw,
        editor = "{J{\"o}rg }Siekmann and Graham Wrightson",
	title = "Automation of Reasoning",
	publisher = "Springer-Verlag",
	address = "New York",
	year = 1983}

@article{urq95,
	author = "Alasdair Urquhart",
	title = "The complexity of propositional proofs",
	journal = "The Bulletin of Symbolic Logic",
	volume = 1,
	pages = "425--467",
	year = 1995}

@incollection{ts70,
	author = "G. S. Tseitin",
	booktitle = "Studies in Constructive Mathematics and Mathematical Logic, Part 2",
	publisher = "Consultants Bureau",
	address = "New York",
	title = "On the complexity of derivation in propositional 
	calculus",
	editor = "A. O. Slisenko",
	pages = "115--125",
	year = 1970
	}