\def\bibRCS{$Id: theory.bib,v 1.405 2002/12/03 19:39:30 beame Exp $}
  \makeatletter \@ifundefined{ccisdefined}{ \newcommand{\cc}[1]{\mbox{\it
  #1\/}} \newcommand{\ccisdefined}{} }{} \@ifundefined{journalfont}{
  \newcommand{\journalfont}{\it } }{} \makeatother
\begin{thebibliography}{49}
\expandafter\ifx\csname natexlab\endcsname\relax\def\natexlab#1{#1}\fi
\expandafter\ifx\csname url\endcsname\relax
  \def\url#1{{\tt #1}}\fi

\bibitem[Achlioptas et~al.(2001)Achlioptas, Beame, and Molloy]{abm:2+psat}
D.~Achlioptas, P.~Beame, and M.~Molloy.
\newblock A sharp threshold in proof complexity.
\newblock In {\em Proceedings of the Thirty-Third Annual ACM Symposium on
  Theory of Computing}, pages 337--346, Crete, Greece, July 2001.

\bibitem[Alekhnovich et~al.(2002)Alekhnovich, Johannsen, Pitassi, and
  Urquhart]{ajpu:regular}
M.~Alekhnovich, J.~Johannsen, T.~Pitassi, and A.~Urquhart.
\newblock An exponential separation between regular and general resolution.
\newblock In {\em Proceedings of the Thirty-Fourth Annual ACM Symposium on
  Theory of Computing}, pages 448--456, Montr\'eal, Canada, May 2002.

\bibitem[Aloul et~al.(2002)Aloul, Ramani, Markov, and
  Sakallah]{arms02:symmetry}
F.~A. Aloul, A.~Ramani, I.~L. Markov, and K.~A. Sakallah.
\newblock Solving difficult {SAT} instances in the presence of symmetry.
\newblock In {\em Proceedings of the 39th Design Automation Conference}, pages
  731--736, New Orleans, LA, June 2002. ACM.

\bibitem[Amir and McIlraith(2000)]{am00}
E.~Amir and S.~A. McIlraith.
\newblock Partition-based logical reasoning.
\newblock In {\em Proceedings of the 7th International Conference on Principles
  of Knowledge Representation and Reasoning}, pages 389--400, Breckenridge, CO,
  Apr. 2000.

\bibitem[Atserias and Bonet(2002)]{ab02:automatizability}
A.~Atserias and M.~L. Bonet.
\newblock On the automatizability of resolution and related propositional proof
  systems.
\newblock In {\em CSL '02: 16th Workshop on Computer Science Logic}, volume
  2471 of {\em Lecture Notes in Computer Science}, pages 569--583, Edinburgh,
  Scotland, Sept. 2002. Springer.

\bibitem[Aziz et~al.(1994)Aziz, Tasiran, and Brayton]{atb94:bddordering}
A.~Aziz, S.~Tasiran, and R.~K. Brayton.
\newblock {BDD} variable orderings for interacting finite state machines.
\newblock In {\em Proceedings of the 31th Design Automation Conference}, pages
  283--288, San Diego, CA, June 1994. ACM.

\bibitem[Baptista and Silva(2000)]{baptista00using}
L.~Baptista and J.~P.~M. Silva.
\newblock Using randomization and learning to solve hard real-world instances
  of satisfiability.
\newblock In {\em 6th Principles and Practice of Constraint Programming}, pages
  489--494, 2000.
\newblock URL \url{citeseer.nj.nec.com/baptista00using.html}.

\bibitem[{Bayardo Jr.} and Schrag(1997)]{rel-sat}
R.~J. {Bayardo Jr.} and R.~C. Schrag.
\newblock Using {CST} look-back techniques to solve real-world {SAT} instances.
\newblock In {\em Proceedings, AAAI-97: 14th National Conference on Artificial
  Intelligence}, pages 203--208, Providence, Rhode Island, July 1997.

\bibitem[Beame et~al.(2003{\natexlab{a}})Beame, Impagliazzo, Pitassi, and
  Segerlind]{bips03:formulacaching}
P.~Beame, R.~Impagliazzo, T.~Pitassi, and N.~Segerlind.
\newblock Memoization and {DPLL}: Formula caching proof systems.
\newblock In {\em Proceedings 18th Annual IEEE Conference on Computational
  Complexity}, pages 225--236, Aarhus, Denmark, July 2003{\natexlab{a}}.

\bibitem[Beame et~al.(2003{\natexlab{b}})Beame, Kautz, and
  Sabharwal]{bks03:learning}
P.~Beame, H.~Kautz, and A.~Sabharwal.
\newblock Understanding the power of clause learning.
\newblock In {\em Proceedings of the 18th International Joint Conference on
  Artificial Intelligence}, pages 1194--1201, Acapulco, Mexico, Aug.
  2003{\natexlab{b}}.

\bibitem[{Ben-Sasson} et~al.(2000){Ben-Sasson}, Impagliazzo, and
  Wigderson]{biw:treeseparation}
E.~{Ben-Sasson}, R.~Impagliazzo, and A.~Wigderson.
\newblock Near-optimal separation of treelike and general resolution.
\newblock Technical Report TR00-005, Electronic Colloquium in Computation
  Complexity, {\tt http://www.eccc.uni-trier.de/eccc/}, 2000.
\newblock To appear in {\em Combinatorica}.

\bibitem[Biere et~al.(1999{\natexlab{a}})Biere, Cimatti, Clarke, Fujita, and
  Zhu]{bccfz99}
A.~Biere, A.~Cimatti, E.~M. Clarke, M.~Fujita, and Y.~Zhu.
\newblock Symbolic model checking using {SAT} procedures instead of {BDDs}.
\newblock In {\em Proceedings of the 36th Design Automation Conference}, pages
  317--320, New Orleans, LA, June 1999{\natexlab{a}}. ACM.

\bibitem[Biere et~al.(1999{\natexlab{b}})Biere, Cimatti, Clarke, and
  Zhu]{bccz99:bmc}
A.~Biere, A.~Cimatti, E.~M. Clarke, and Y.~Zhu.
\newblock Symbolic model checking without {BDDs}.
\newblock In {\em 5th International Conference on Tools and Algorithms for the
  Construction and Analysis of Systems}, pages 193--207, Amsterdam, the
  Netherlands, Mar. 1999{\natexlab{b}}.

\bibitem[Bonet et~al.(2000)Bonet, Esteban, Galesi, and Johansen]{begj}
M.~L. Bonet, J.~L. Esteban, N.~Galesi, and J.~Johansen.
\newblock On the relative complexity of resolution refinements and cutting
  planes proof systems.
\newblock {\em SIAM Journal on Computing}, 30\penalty0 (5):\penalty0
  1462--1484, 2000.

\bibitem[Bonet and Galesi(2001)]{bg01:optimality}
M.~L. Bonet and N.~Galesi.
\newblock Optimality of size-width tradeoffs for resolution.
\newblock {\em Computational Complexity}, 10\penalty0 (4):\penalty0 261--276,
  2001.

\bibitem[Brafman(2001)]{2simplify}
R.~I. Brafman.
\newblock A simplifier for propositional formulas with many binary clauses.
\newblock In {\em Proceedings of the 17th International Joint Conference on
  Artificial Intelligence}, pages 515--522, Seattle, WA, Aug. 2001.

\bibitem[{Buresh-Oppenheim} and Pitassi(2003)]{bt03:refinements}
J.~{Buresh-Oppenheim} and T.~Pitassi.
\newblock The complexity of resolution refinements.
\newblock In {\em 18th Annual IEEE Symposium on Logic in Computer Science},
  pages 138--147, Ottawa, Canada, June 2003.

\bibitem[Cook and Reckhow(1977)]{cr77}
S.~A. Cook and R.~A. Reckhow.
\newblock The relative efficiency of propositional proof systems.
\newblock {\em Journal of Symbolic Logic}, 44\penalty0 (1):\penalty0 36--50,
  1977.

\bibitem[Davis et~al.(1962)Davis, Logemann, and Loveland]{dll:prover}
M.~Davis, G.~Logemann, and D.~Loveland.
\newblock A machine program for theorem proving.
\newblock {\em Communications of the ACM}, 5:\penalty0 394--397, 1962.

\bibitem[Davis and Putnam(1960)]{dp:prover}
M.~Davis and H.~Putnam.
\newblock A computing procedure for quantification theory.
\newblock {\em Communications of the ACM}, 7:\penalty0 201--215, 1960.

\bibitem[Davis(1984)]{davis84diagnostic}
R.~Davis.
\newblock Diagnostic reasoning based on structure and behavior.
\newblock {\em Artificial Intelligence}, 24:\penalty0 347--410, 1984.

\bibitem[de~Kleer and Williams(1987)]{kleer87diagnosing}
J.~de~Kleer and B.~C. Williams.
\newblock Diagnosing multiple faults.
\newblock {\em Artificial Intelligence}, 32\penalty0 (1):\penalty0 97--130,
  1987.

\bibitem[Esteban et~al.(2002)Esteban, Galesi, and Messner]{egm02:boundedResK}
J.~L. Esteban, N.~Galesi, and J.~Messner.
\newblock On the complexity of resolution with bounded conjunctions.
\newblock In {\em Automata, Languages, and Programming: 29th International
  Colloquium}, volume 2380 of {\em Lecture Notes in Computer Science}, pages
  220--231, Malaga, Spain, July 2002. Springer-Verlag.

\bibitem[Genesereth(1984)]{genesereth84design}
R.~Genesereth.
\newblock The use of design descriptions in automated diagnosis.
\newblock {\em Artificial Intelligence}, 24:\penalty0 411--436, 1984.

\bibitem[Giunchiglia et~al.(2002)Giunchiglia, Maratea, and Tacchella]{ivs}
E.~Giunchiglia, M.~Maratea, and A.~Tacchella.
\newblock Dependent and independent variables in propositional satisfiability.
\newblock In {\em Proceedings of the 8th European Conference on Logics in
  Artificial Intelligence (JELIA)}, volume 2424 of {\em Lecture Notes in
  Computer Science}, pages 296--307, Cosenza, Italy, Sept. 2002.
  Springer-Verlag.

\bibitem[Gomes et~al.(1998{\natexlab{a}})Gomes, Selman, and
  Kautz]{gomes98boosting}
C.~P. Gomes, B.~Selman, and H.~Kautz.
\newblock Boosting combinatorial search through randomization.
\newblock In {\em Proceedings, AAAI-98: 15th National Conference on Artificial
  Intelligence}, pages 431--437, Madison, WI, 1998{\natexlab{a}}.
\newblock URL \url{citeseer.nj.nec.com/gomes98boosting.html}.

\bibitem[Gomes et~al.(1998{\natexlab{b}})Gomes, Selman, McAloon, and
  Tretkoff]{sat:scheduling}
C.~P. Gomes, B.~Selman, K.~McAloon, and C.~Tretkoff.
\newblock Randomization in backtrack search: Exploiting heavy-tailed profiles
  for solving hard scheduling problems.
\newblock In {\em Proceedings of the 4th International Conference on Artificial
  Intelligence Planning Systems}, Pittsburgh, PA, June 1998{\natexlab{b}}.

\bibitem[Haken(1985)]{haken:pigeon}
A.~Haken.
\newblock The intractability of resolution.
\newblock {\em Theoretical Computer Science}, 39:\penalty0 297--305, 1985.

\bibitem[Harlow and Brglez(1998)]{hb98}
J.~E. Harlow and F.~Brglez.
\newblock Design of experiments in {BDD} variable ordering: Lessons learned.
\newblock In {\em Proceedings of the International Conference on Computer Aided
  Design}, pages 646--652, San Jose, CA, Nov. 1998. IEEE/ACM.

\bibitem[Johnson and Trick(1996)]{seconddimacschallenge}
D.~S. Johnson and M.~A. Trick, editors.
\newblock {\em Cliques, Coloring and Satisfiability: Second {DIMACS}
  Implementation Challenge}, volume~26 of {\em {DIMACS} Series in Discrete
  Mathematics and Theoretical Computer Science}.
\newblock AMS, 1996.

\bibitem[Kautz and Selman(1992)]{ks92}
H.~A. Kautz and B.~Selman.
\newblock Planning as satisfiability.
\newblock In {\em Proceedings of the 10th European Conference on Artificial
  Intelligence}, pages 359--363, Vienna, Austria, Aug. 1992.

\bibitem[Kautz and Selman(1996)]{ks96}
H.~A. Kautz and B.~Selman.
\newblock Pushing the envelope: Planning, propositional logic, and stochastic
  search.
\newblock In {\em Proceedings, AAAI-96: 13th National Conference on Artificial
  Intelligence}, pages 1194--1201, Portland, OR, Aug. 1996.

\bibitem[Konuk and Larrabee(1993)]{kl93}
H.~Konuk and T.~Larrabee.
\newblock Explorations of sequential {ATPG} using boolean satisfiability.
\newblock In {\em 11th VLSI Test Symposium}, pages 85--90, 1993.

\bibitem[Kraj\'{\i}\v{c}ek(2001)]{krajicek01:wphp}
J.~Kraj\'{\i}\v{c}ek.
\newblock On the weak pigeonhole principle.
\newblock {\em Fundamenta Mathematicae}, 170\penalty0 (1-3):\penalty0 123--140,
  2001.

\bibitem[Krishnamurthy(1985)]{krishnamurthy85}
B.~Krishnamurthy.
\newblock Short proofs for tricky formulas.
\newblock {\em Acta Informatica}, 22:\penalty0 253--274, 1985.

\bibitem[Li and Anbulagan(1997)]{satz}
C.~M. Li and Anbulagan.
\newblock Heuristics based on unit propagation for satisfiability problems.
\newblock In {\em Proceedings of the 15th International Joint Conference on
  Artificial Intelligence}, pages 366--371, Nagoya, Japan, Aug. 1997.
\newblock URL \url{citeseer.nj.nec.com/li97heuristics.html}.

\bibitem[Marques-Silva(1998)]{silva98:resolve}
J.~Marques-Silva.
\newblock An overview of backtrack search satisfiability algorithms.
\newblock In {\em 5th International Symposium on Artificial Intelligence and
  Mathematics}, Fort Lauderdale, Florida, Jan. 1998.

\bibitem[Marques-Silva and Sakallah(1996)]{grasp}
J.~P. Marques-Silva and K.~A. Sakallah.
\newblock {GRASP} -- a new search algorithm for satisfiability.
\newblock In {\em Proceedings of the International Conference on Computer Aided
  Design}, pages 220--227, San Jose, CA, Nov. 1996. ACM/IEEE.

\bibitem[M\'{e}zard and Zecchina(2002)]{surveyprop}
M.~M\'{e}zard and R.~Zecchina.
\newblock Random k-satisfiability problem: From an analytic solution to an
  efficient algorithm.
\newblock {\em Physical Review E}, 66:\penalty0 056126, Nov. 2002.

\bibitem[Moskewicz et~al.(2001)Moskewicz, Madigan, Zhao, Zhang, and
  Malik]{chaff}
M.~W. Moskewicz, C.~F. Madigan, Y.~Zhao, L.~Zhang, and S.~Malik.
\newblock Chaff: Engineering an efficient {SAT} solver.
\newblock In {\em Proceedings of the 38th Design Automation Conference}, pages
  530--535, Las Vegas, NV, June 2001. ACM.

\bibitem[Ostrowski et~al.(2002)Ostrowski, Gr\'{e}goire, Mazure, and Sais]{lsat}
R.~Ostrowski, E.~Gr\'{e}goire, B.~Mazure, and L.~Sais.
\newblock Recovering and exploiting structural knowledge from cnf formulas.
\newblock In {\em 8th Principles and Practice of Constraint Programming},
  volume 2470 of {\em Lecture Notes in Computer Science}, pages 185--199,
  Ithaca, NY, Sept. 2002. Springer-Verlag.

\bibitem[Reda et~al.(2002)Reda, Drechsler, and Orailoglu]{rdo02:bddsat}
S.~Reda, R.~Drechsler, and A.~Orailoglu.
\newblock On the relation between {SAT} and {BDD}s for equivalence checking.
\newblock In {\em Proceedings of the International Symposium on Quality
  Electronic Design}, pages 394--399, San Jose, CA, Mar. 2002.

\bibitem[Sabharwal et~al.(2003)Sabharwal, Beame, and Kautz]{sbk03:structure}
A.~Sabharwal, P.~Beame, and H.~Kautz.
\newblock Using problem structure for efficient clause learning.
\newblock In {\em Proceedings of the 6th International Conference on Theory and
  Applications of Satisfiability Testing}, volume 2919 of {\em Lecture Notes in
  Computer Science}, pages 242--256, Portofino, Italy, May 2003.
  Springer-Verlag.

\bibitem[Shtrichman(2000)]{shtrichman00}
O.~Shtrichman.
\newblock Tuning {SAT} checkers for bounded model checking.
\newblock In {\em Proceedings of the 12th International Conference on Computer
  Aided Verification}, pages 480--494, Chicago, IL, July 2000.

\bibitem[Stallman and Sussman(1977)]{stallman77forward}
R.~Stallman and G.~J. Sussman.
\newblock Forward reasoning and dependency-directed backtracking in a system
  for computer-aided circuit analysis.
\newblock {\em Artificial Intelligence}, 9:\penalty0 135--196, 1977.

\bibitem[Velev and Bryant(2001)]{velev01Effective}
M.~Velev and R.~Bryant.
\newblock Effective use of boolean satisfiability procedures in the formal
  verification of superscalar and vliw microprocessors.
\newblock In {\em Proceedings of the 38th Design Automation Conference}, pages
  226--231, 2001.

\bibitem[Zhang(1997)]{sato}
H.~Zhang.
\newblock {SATO}: An efficient propositional prover.
\newblock In {\em Proceedings of the 14th International Conference on Automated
  Deduction}, volume 1249 of {\em Lecture Notes in Computer Science}, pages
  272--275, Townsville, Australia, July 1997.

\bibitem[Zhang and Hsiang(1994)]{zh94}
H.~Zhang and J.~Hsiang.
\newblock Solving open quasigroup problems by propositional reasoning.
\newblock In {\em Proceedings of the International Computer Symp.}, Hsinchu,
  Taiwan, 1994.

\bibitem[Zhang et~al.(2001)Zhang, Madigan, Moskewicz, and
  Malik]{zchaff:learning_schemes}
L.~Zhang, C.~F. Madigan, M.~H. Moskewicz, and S.~Malik.
\newblock Efficient conflict driven learning in a boolean satisfiability
  solver.
\newblock In {\em Proceedings of the International Conference on Computer Aided
  Design}, pages 279--285, San Jose, CA, Nov. 2001. IEEE/ACM.

\end{thebibliography}
