\begin{thebibliography}{}

\bibitem[\protect\BCAY{Aloul, Ramani, Markov,\ \BBA\ Sakallah}{Aloul
  et~al.}{2002}]{Aloul:PBS}
Aloul, F., Ramani, A., Markov, I., \BBA\ Sakallah, K. \BBOP2002\BBCP.
\newblock \BBOQ {PBS}: A backtrack search pseudo-{B}oolean solver\BBCQ\
\newblock In {\Bem Symposium on the Theory and Applications of Satisfiability
  Testing}.

\bibitem[\protect\BCAY{Babai}{Babai}{1995}]{Babai95}
Babai, L. \BBOP1995\BBCP.
\newblock \BBOQ Automorphism groups, isomorphism, reconstruction\BBCQ\
\newblock In Lov\'asz, L., Graham, R., \BBA\ Gr\"otschel, M.\BEDS, {\Bem
  Handbook for Combinatorics}, \BCH~27, \BPGS\ 1447--1540.
  North-Holland-Elsevier.

\bibitem[\protect\BCAY{Baker}{Baker}{1994}]{Baker:fancy}
Baker, A.~B. \BBOP1994\BBCP.
\newblock \BBOQ The hazards of fancy backtracking\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth National Conference on Artificial
  Intelligence}.

\bibitem[\protect\BCAY{Barth}{Barth}{1995}]{Barth:pseudo}
Barth, P. \BBOP1995\BBCP.
\newblock \BBOQ A {D}avis-{P}utnam based enumeration algorithm for linear
  pseudo-boolean optimization\BBCQ\
\newblock \BTR\ MPI-I-95-2-003, Max Planck Institut f\"ur Informatik,
  Saarbr\"ucken, Germany.

\bibitem[\protect\BCAY{Barth}{Barth}{1996}]{Barth:01}
Barth, P. \BBOP1996\BBCP.
\newblock {\Bem Logic-Based 0-1 Constraint Programming}, \lowercase{\BVOL}~5 of
  {\Bem Operations Research/Computer Science Interfaces Series}.
\newblock Kluwer.

\bibitem[\protect\BCAY{Baumgartner}{Baumgartner}{2000}]{Baumgartner:fdpll}
Baumgartner, P. \BBOP2000\BBCP.
\newblock \BBOQ {FDPLL -- A First-Order Davis-Putnam-Logeman-Loveland
  Procedure}\BBCQ\
\newblock In McAllester, D.\BED, {\Bem {CADE}-17 -- The 17th International
  Conference on Automated Deduction}, \lowercase{\BVOL}\ 1831, \BPGS\ 200--219.
  Springer.

\bibitem[\protect\BCAY{Bayardo\ \BBA\ Miranker}{Bayardo\ \BBA\
  Miranker}{1996}]{Bayardo:relsat}
Bayardo, R.~J.\BBACOMMA\  \BBA\ Miranker, D.~P. \BBOP1996\BBCP.
\newblock \BBOQ A complexity analysis of space-bounded learning algorithms for
  the constraint satisfaction problem\BBCQ\
\newblock In {\Bem Proceedings of the Thirteenth National Conference on
  Artificial Intelligence}, \BPGS\ 298--304.

\bibitem[\protect\BCAY{Bayardo\ \BBA\ Schrag}{Bayardo\ \BBA\
  Schrag}{1997}]{Schrag:relsat}
Bayardo, R.~J.\BBACOMMA\  \BBA\ Schrag, R.~C. \BBOP1997\BBCP.
\newblock \BBOQ Using {CSP} look-back techniques to solve real-world {SAT}
  instances\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth National Conference on
  Artificial Intelligence}, \BPGS\ 203--208.

\bibitem[\protect\BCAY{Beame\ \BBA\ Pitassi}{Beame\ \BBA\
  Pitassi}{2001}]{Beame:complexity}
Beame, P.\BBACOMMA\  \BBA\ Pitassi, T. \BBOP2001\BBCP.
\newblock \BBOQ Propositional proof complexity: Past, present and future\BBCQ\
\newblock In Paun, G., Rozenberg, G., \BBA\ Salomaa, A.\BEDS, {\Bem Current
  Trends in Theoretical Computer Science, Entering the 21th Century}, \BPGS\
  42--70. World Scientific.

\bibitem[\protect\BCAY{Benhamou, Sais,\ \BBA\ Siegel}{Benhamou
  et~al.}{1994}]{benhamou:dpc}
Benhamou, B., Sais, L., \BBA\ Siegel, P. \BBOP1994\BBCP.
\newblock \BBOQ Two proof procedures for a cardinality based language in
  propositional calculus\BBCQ\
\newblock In {\Bem Proceedings of STACS94, volume 775 de Lecture Notes in
  Computer Science}.

\bibitem[\protect\BCAY{Biere, Clarke, Raimi,\ \BBA\ Zhu}{Biere
  et~al.}{1999}]{Biere:verify}
Biere, A., Clarke, E., Raimi, R., \BBA\ Zhu, Y. \BBOP1999\BBCP.
\newblock \BBOQ Verifying safety properties of a {PowerPC} microprocessor using
  symbolic model checking without {BDDs}\BBCQ\
\newblock {\Bem Lecture Notes in Computer Science}, {\Bem 1633}.

\bibitem[\protect\BCAY{Bonet, Pitassi,\ \BBA\ Raz}{Bonet
  et~al.}{1997}]{bonet-pb-clique}
Bonet, M.~L., Pitassi, T., \BBA\ Raz, R. \BBOP1997\BBCP.
\newblock \BBOQ Lower bounds for cutting planes proofs with small
  coefficients\BBCQ\
\newblock {\Bem Journal of Symbolic Logic}, {\Bem 62\/}(3), 708--728.

\bibitem[\protect\BCAY{Brown, Finkelstein,\ \BBA\ Paul Walton~Purdom}{Brown
  et~al.}{1988}]{Brown:symmetry}
Brown, C.~A., Finkelstein, L., \BBA\ Paul Walton~Purdom, J. \BBOP1988\BBCP.
\newblock \BBOQ Backtrack searching in the presence of symmetry\BBCQ\
\newblock In Mora, T.\BED, {\Bem Applied Algebra, Algebraic Algorithms and
  Error-Correcting Codes, 6th Int'l. Conf.}, \BPGS\ 99--110. Springer-Verlag.

\bibitem[\protect\BCAY{Bryant}{Bryant}{1986}]{Bryant:bdd1}
Bryant, R.~E. \BBOP1986\BBCP.
\newblock \BBOQ Graph-based algorithms for {B}oolean function
  manipulation\BBCQ\
\newblock {\Bem IEEE Transactions on Computers}, {\Bem C-35\/}(8), 677--691.

\bibitem[\protect\BCAY{Bryant}{Bryant}{1992}]{Bryant:bdd2}
Bryant, R.~E. \BBOP1992\BBCP.
\newblock \BBOQ Symbolic {Boolean} manipulation with ordered binary-decision
  diagrams\BBCQ\
\newblock {\Bem ACM Computing Surveys}, {\Bem 24\/}(3), 293--318.

\bibitem[\protect\BCAY{Buchberger}{Buchberger}{1965}]{Groebner65}
Buchberger, B. \BBOP1965\BBCP.
\newblock {\Bem Ein {A}lgorithmus zum {A}uffinden der {B}asiselemente des
  {R}estklassenringes nach einum nulldimensionalen {P}olynomideal}.
\newblock Ph.D.\ thesis, University of Innsbruck, Innsbruck.

\bibitem[\protect\BCAY{Buchberger}{Buchberger}{1985}]{Groebner85}
Buchberger, B. \BBOP1985\BBCP.
\newblock \BBOQ Gr\"obner bases: An algorithmic method in polynomial ideal
  theory\BBCQ\
\newblock In Bose, N.\BED, {\Bem Multidimensional Systems Theory}. D. Reidel,
  Dordrecht, Holland.

\bibitem[\protect\BCAY{Cadoli, Schaerf, Giovanardi,\ \BBA\ Giovanardi}{Cadoli
  et~al.}{2002}]{Cadoli:qbf}
Cadoli, M., Schaerf, M., Giovanardi, A., \BBA\ Giovanardi, M. \BBOP2002\BBCP.
\newblock \BBOQ An algorithm to evaluate quantified boolean formulae and its
  experimental evaluation\BBCQ\
\newblock {\Bem Journal of Automated Reasoning}, {\Bem 28\/}(2), 101--142.

\bibitem[\protect\BCAY{Chai\ \BBA\ Kuehlmann}{Chai\ \BBA\
  Kuehlmann}{2003}]{Chai:pb}
Chai, D.\BBACOMMA\  \BBA\ Kuehlmann, A. \BBOP2003\BBCP.
\newblock \BBOQ A fast pseudo-{B}oolean constraint solver\BBCQ\
\newblock In {\Bem Proceedings of the 40th Design Automation Conference},
  \BPGS\ 830--835.

\bibitem[\protect\BCAY{Chandru\ \BBA\ Hooker}{Chandru\ \BBA\
  Hooker}{1999}]{Chandru:logic_book}
Chandru, V.\BBACOMMA\  \BBA\ Hooker, J.~N. \BBOP1999\BBCP.
\newblock {\Bem Optimization Mehtods for Logical Inference}.
\newblock Wiley-Interscience.

\bibitem[\protect\BCAY{Clegg, Edmonds,\ \BBA\ Impagliazzo}{Clegg
  et~al.}{1996}]{Clegg:Groebner}
Clegg, M., Edmonds, J., \BBA\ Impagliazzo, R. \BBOP1996\BBCP.
\newblock \BBOQ Using the {Groebner} basis algorithm to find proofs of
  unsatisfiability\BBCQ\
\newblock In {\Bem Proceedings of the Twenty-Eighth Annual {ACM} Symp. on
  Theory of Computing}, \BPGS\ 174--183.

\bibitem[\protect\BCAY{Coarfa, Demopoulos, {San Miguel Aguirre}, Subramanian,\
  \BBA\ Vardi}{Coarfa et~al.}{2000}]{Coarfa:3sat}
Coarfa, C., Demopoulos, D.~D., {San Miguel Aguirre}, A., Subramanian, D., \BBA\
  Vardi, M. \BBOP2000\BBCP.
\newblock \BBOQ Random {3-{SAT}}: The plot thickens\BBCQ\
\newblock In {\Bem Proceedings of the International Conference on Constraint
  Programming}.

\bibitem[\protect\BCAY{Cook}{Cook}{1971}]{Cook:sat}
Cook, S.~A. \BBOP1971\BBCP.
\newblock \BBOQ The complexity of theorem-proving procedures\BBCQ\
\newblock In {\Bem Proceedings of the 3rd Annual ACM Symposium on the Theory of
  Computing}, \BPGS\ 151--158.

\bibitem[\protect\BCAY{Cook, Coullard,\ \BBA\ Turan}{Cook
  et~al.}{1987}]{Cook:php}
Cook, W., Coullard, C., \BBA\ Turan, G. \BBOP1987\BBCP.
\newblock \BBOQ On the complexity of cutting-plane proofs\BBCQ\
\newblock {\Bem Discrete Applied Mathematics}, {\Bem 18}, 25--38.

\bibitem[\protect\BCAY{Copty, Fix, Giunchiglia, Kamhi, Tacchella,\ \BBA\
  Vardi}{Copty et~al.}{2001}]{sat-mtv}
Copty, F., Fix, L., Giunchiglia, E., Kamhi, G., Tacchella, A., \BBA\ Vardi, M.
  \BBOP2001\BBCP.
\newblock \BBOQ Benefits of bounded model checking in an industrial
  setting\BBCQ\
\newblock In {\Bem 13th Conference on Computer Aided Verification, {CAV'01}},
  Paris, France.

\bibitem[\protect\BCAY{Crawford}{Crawford}{1992}]{Crawford:symmetry}
Crawford, J.~M. \BBOP1992\BBCP.
\newblock \BBOQ A theoretical analysis of reasoning by symmetry in first-order
  logic (extended abstract)\BBCQ\
\newblock In {\Bem AAAI Workshop on Tractable Reasoning}.

\bibitem[\protect\BCAY{Crawford\ \BBA\ Auton}{Crawford\ \BBA\
  Auton}{1996}]{Crawford:exp}
Crawford, J.~M.\BBACOMMA\  \BBA\ Auton, L.~D. \BBOP1996\BBCP.
\newblock \BBOQ Experimental results on the crossover point in random
  {3SAT}\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 81}, 31--57.

\bibitem[\protect\BCAY{Crawford, Ginsberg, Luks,\ \BBA\ Roy}{Crawford
  et~al.}{1996}]{Ginsberg:symmetry}
Crawford, J.~M., Ginsberg, M.~L., Luks, E., \BBA\ Roy, A. \BBOP1996\BBCP.
\newblock \BBOQ Symmetry breaking predicates for search problems\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Conference on
  Principles of Knowledge Representation and Reasoning}, Boston, MA.

\bibitem[\protect\BCAY{Davis\ \BBA\ Putnam}{Davis\ \BBA\
  Putnam}{1960}]{Davis-Putnam}
Davis, M.\BBACOMMA\  \BBA\ Putnam, H. \BBOP1960\BBCP.
\newblock \BBOQ A computing procedure for quantification theory\BBCQ\
\newblock {\Bem J. Assoc. Comput. Mach.}, {\Bem 7}, 201--215.

\bibitem[\protect\BCAY{Davis, Logemann,\ \BBA\ Loveland}{Davis
  et~al.}{1962}]{DPLL}
Davis, M., Logemann, G., \BBA\ Loveland, D. \BBOP1962\BBCP.
\newblock \BBOQ A machine program for theorem-proving\BBCQ\
\newblock {\Bem Communications of the ACM}, {\Bem 5\/}(7), 394--397.

\bibitem[\protect\BCAY{Dechter}{Dechter}{1990}]{Dechter:bj}
Dechter, R. \BBOP1990\BBCP.
\newblock \BBOQ Enhancement schemes for constraint processing: Backjumping,
  learning, and cutset decomposition\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 41}, 273--312.

\bibitem[\protect\BCAY{Dixon\ \BBA\ Ginsberg}{Dixon\ \BBA\
  Ginsberg}{2000}]{Dixon:AIOR}
Dixon, H.~E.\BBACOMMA\  \BBA\ Ginsberg, M.~L. \BBOP2000\BBCP.
\newblock \BBOQ Combining satisfiability techniques from {AI} and {OR}\BBCQ\
\newblock {\Bem Knowledge Engrg. Rev.}, {\Bem 15}, 31--45.

\bibitem[\protect\BCAY{Dixon\ \BBA\ Ginsberg}{Dixon\ \BBA\
  Ginsberg}{2002}]{Dixon:strengthen}
Dixon, H.~E.\BBACOMMA\  \BBA\ Ginsberg, M.~L. \BBOP2002\BBCP.
\newblock \BBOQ Inference methods for a pseudo-{B}oolean satisfiability
  solver\BBCQ\
\newblock In {\Bem Proceedings of the Eighteenth National Conference on
  Artificial Intelligence}.

\bibitem[\protect\BCAY{Dixon, Ginsberg, Hofer, Luks,\ \BBA\ Parkes}{Dixon
  et~al.}{2003a}]{Ginsberg:zap3}
Dixon, H.~E., Ginsberg, M.~L., Hofer, D., Luks, E.~M., \BBA\ Parkes, A.~J.
  \BBOP2003a\BBCP.
\newblock \BBOQ Generalizing {B}oolean satisfiability {III}:
  {I}mplementation\BBCQ\
\newblock \BTR, Computational Intelligence Research Laboratory, Eugene, Oregon.

\bibitem[\protect\BCAY{Dixon, Ginsberg, Luks,\ \BBA\ Parkes}{Dixon
  et~al.}{2003b}]{Ginsberg:zap2}
Dixon, H.~E., Ginsberg, M.~L., Luks, E.~M., \BBA\ Parkes, A.~J.
  \BBOP2003b\BBCP.
\newblock \BBOQ Generalizing {B}oolean satisfiability {II}: {T}heory\BBCQ\
\newblock \BTR, Computational Intelligence Research Laboratory, Eugene, Oregon.

\bibitem[\protect\BCAY{Dubois, Andre, Boufkhad,\ \BBA\ Carlier}{Dubois
  et~al.}{1993}]{Dubois:branch}
Dubois, O., Andre, P., Boufkhad, Y., \BBA\ Carlier, J. \BBOP1993\BBCP.
\newblock \BBOQ {SAT} versus {UNSAT}\BBCQ\
\newblock In {\Bem Second DIMACS Challenge: Cliques, Colorings and
  Satisfiability}, Rutgers University, NJ.

\bibitem[\protect\BCAY{Dubois\ \BBA\ Dequen}{Dubois\ \BBA\
  Dequen}{2001}]{Dubois:backbone}
Dubois, O.\BBACOMMA\  \BBA\ Dequen, G. \BBOP2001\BBCP.
\newblock \BBOQ A backbone-search heuristic for efficient solving of hard
  3-{SAT} formulae\BBCQ\
\newblock In {\Bem Proceedings of the Seventeenth International Joint
  Conference on Artificial Intelligence}, \BPGS\ 248--253.

\bibitem[\protect\BCAY{East\ \BBA\ Truszczy{\'n}ski}{East\ \BBA\
  Truszczy{\'n}ski}{2001}]{East:propositional}
East, D.\BBACOMMA\  \BBA\ Truszczy{\'n}ski, M. \BBOP2001\BBCP.
\newblock \BBOQ Propositional satisfiability in answer-set programming\BBCQ\
\newblock {\Bem Lecture Notes in Computer Science}, {\Bem 2174}.

\bibitem[\protect\BCAY{East\ \BBA\ Truszczy{\'n}ski}{East\ \BBA\
  Truszczy{\'n}ski}{2002}]{East:PS}
East, D.\BBACOMMA\  \BBA\ Truszczy{\'n}ski, M. \BBOP2002\BBCP.
\newblock \BBOQ Propositional satisfiability in declarative programming\BBCQ\
\newblock Extended version of papers that appeared in Proceedings of AAAI-2000
  and Proceedings of KI-2001. http://xxx.lanl.gov/abs/cs.LO/0211033.

\bibitem[\protect\BCAY{Freeman}{Freeman}{1995}]{Freeman:SAT}
Freeman, J.~W. \BBOP1995\BBCP.
\newblock {\Bem Improvements to propositional satisfiability search
  algorithms}.
\newblock Ph.D.\ thesis, University of Pennsylvania, PA.

\bibitem[\protect\BCAY{Frost\ \BBA\ Dechter}{Frost\ \BBA\
  Dechter}{1994}]{Dechter:length}
Frost, D.\BBACOMMA\  \BBA\ Dechter, R. \BBOP1994\BBCP.
\newblock \BBOQ Dead-end driven learning\BBCQ\
\newblock In {\Bem Proceedings of the Twelfth National Conference on Artificial
  Intelligence}, \BPGS\ 294--300.

\bibitem[\protect\BCAY{Galperin\ \BBA\ Wigderson}{Galperin\ \BBA\
  Wigderson}{1983}]{smallok}
Galperin, H.\BBACOMMA\  \BBA\ Wigderson, A. \BBOP1983\BBCP.
\newblock \BBOQ Succinct representation of graphs\BBCQ\
\newblock {\Bem Information and Control}, {\Bem 56}, 183--198.

\bibitem[\protect\BCAY{Garey\ \BBA\ Johnson}{Garey\ \BBA\
  Johnson}{1979}]{Garey&Johnson}
Garey, M.\BBACOMMA\  \BBA\ Johnson, D. \BBOP1979\BBCP.
\newblock {\Bem Computers and Intractability}.
\newblock W.H. Freeman and Co., New York.

\bibitem[\protect\BCAY{Gaschnig}{Gaschnig}{1979}]{Gaschnig:bj}
Gaschnig, J. \BBOP1979\BBCP.
\newblock \BBOQ Performance measurement and analysis of certain search
  algorithms\BBCQ\
\newblock \BTR\ CMU-CS-79-124, Carnegie-Mellon University.

\bibitem[\protect\BCAY{Gelfond\ \BBA\ Lifschitz}{Gelfond\ \BBA\
  Lifschitz}{1988}]{Gelfond:stable}
Gelfond, M.\BBACOMMA\  \BBA\ Lifschitz, V. \BBOP1988\BBCP.
\newblock \BBOQ The stable semantics for logic programs\BBCQ\
\newblock In {\Bem Proceedings of the 5th International Conference on Logic
  Programming}, \BPGS\ 1070--1080. MIT Press.

\bibitem[\protect\BCAY{Ginsberg}{Ginsberg}{1993}]{Ginsberg:dynamic}
Ginsberg, M.~L. \BBOP1993\BBCP.
\newblock \BBOQ Dynamic backtracking\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 1}, 25--46.

\bibitem[\protect\BCAY{Ginsberg\ \BBA\ Geddis}{Ginsberg\ \BBA\
  Geddis}{1991}]{Ginsberg:metalevel}
Ginsberg, M.~L.\BBACOMMA\  \BBA\ Geddis, D.~F. \BBOP1991\BBCP.
\newblock \BBOQ Is there any need for domain-dependent control
  information?\BBCQ\
\newblock In {\Bem Proceedings of the Ninth National Conference on Artificial
  Intelligence}.

\bibitem[\protect\BCAY{Ginsberg\ \BBA\ Parkes}{Ginsberg\ \BBA\
  Parkes}{2000}]{Ginsberg:qprop}
Ginsberg, M.~L.\BBACOMMA\  \BBA\ Parkes, A.~J. \BBOP2000\BBCP.
\newblock \BBOQ Search, subsearch and {QPROP}\BBCQ\
\newblock In {\Bem Proceedings of the Seventh International Conference on
  Principles of Knowledge Representation and Reasoning}, Breckenridge,
  Colorado.

\bibitem[\protect\BCAY{Goldberg\ \BBA\ Novikov}{Goldberg\ \BBA\
  Novikov}{2002}]{berkmin}
Goldberg, E.\BBACOMMA\  \BBA\ Novikov, Y. \BBOP2002\BBCP.
\newblock \BBOQ Berkmin: A fast and robust {SAT} solver\BBCQ\
\newblock In {\Bem Design Automation and Test in Europe (DATE)}, \BPGS\
  142--149.

\bibitem[\protect\BCAY{Guignard\ \BBA\ Spielberg}{Guignard\ \BBA\
  Spielberg}{1981}]{Guignard:strengthening}
Guignard, M.\BBACOMMA\  \BBA\ Spielberg, K. \BBOP1981\BBCP.
\newblock \BBOQ Logical reduction methods in zero-one programming\BBCQ\
\newblock {\Bem Operations Research}, {\Bem 29}.

\bibitem[\protect\BCAY{Haken}{Haken}{1985}]{Haken}
Haken, A. \BBOP1985\BBCP.
\newblock \BBOQ The intractability of resolution\BBCQ\
\newblock {\Bem Theoretical Computer Science}, {\Bem 39}, 297--308.

\bibitem[\protect\BCAY{Haken}{Haken}{1995}]{Haken:mosquito}
Haken, A. \BBOP1995\BBCP.
\newblock \BBOQ Counting bottlenecks to show monotone {$P\neq NP$}\BBCQ\
\newblock In {\Bem Proceedings 36th Annual IEEE Symp. on Foundations of
  Computer Science (FOCS-95)}, \BPGS\ 36--40, Milwaukee, MN. IEEE.

\bibitem[\protect\BCAY{Hooker}{Hooker}{1988}]{Hooker:genres}
Hooker, J.~N. \BBOP1988\BBCP.
\newblock \BBOQ Generalized resolution and cutting planes\BBCQ\
\newblock {\Bem Annals of Operations Research}, {\Bem 12}, 217--239.

\bibitem[\protect\BCAY{Hooker\ \BBA\ Vinay}{Hooker\ \BBA\
  Vinay}{1995}]{Hooker:branching}
Hooker, J.~N.\BBACOMMA\  \BBA\ Vinay, V. \BBOP1995\BBCP.
\newblock \BBOQ Branching rules for satisfiability\BBCQ\
\newblock {\Bem J. Automated Reasoning}, {\Bem 15}, 359--383.

\bibitem[\protect\BCAY{Jeroslow\ \BBA\ Wang}{Jeroslow\ \BBA\
  Wang}{1990}]{Jeroslow:branching}
Jeroslow, R.\BBACOMMA\  \BBA\ Wang, J. \BBOP1990\BBCP.
\newblock \BBOQ Solving the propositional satisfiability problem\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 1},
  167--187.

\bibitem[\protect\BCAY{Joslin\ \BBA\ Roy}{Joslin\ \BBA\
  Roy}{1997}]{Joslin:symmetry}
Joslin, D.\BBACOMMA\  \BBA\ Roy, A. \BBOP1997\BBCP.
\newblock \BBOQ Exploiting symmetry in lifted {CSP}s\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth National Conference on
  Artificial Intelligence}, \BPGS\ 197--202.

\bibitem[\protect\BCAY{Kautz\ \BBA\ Selman}{Kautz\ \BBA\
  Selman}{1998}]{Selman:blackbox}
Kautz, H.\BBACOMMA\  \BBA\ Selman, B. \BBOP1998\BBCP.
\newblock \BBOQ {BLACKBOX}: {A} new approach to the application of theorem
  proving to problem solving\BBCQ\
\newblock In {\Bem Artificial Intelligence Planning Systems: Proceedings of the
  Fourth International Conference}. AAAI Press.

\bibitem[\protect\BCAY{Kautz\ \BBA\ Selman}{Kautz\ \BBA\
  Selman}{1992}]{satplan}
Kautz, H.~A.\BBACOMMA\  \BBA\ Selman, B. \BBOP1992\BBCP.
\newblock \BBOQ Planning as satisfiability\BBCQ\
\newblock In {\Bem Proceedings of the Tenth European Conference on Artificial
  Intelligence ({ECAI}'92)}, \BPGS\ 359--363.

\bibitem[\protect\BCAY{Kirkpatrick\ \BBA\ Selman}{Kirkpatrick\ \BBA\
  Selman}{1994}]{Selman:science}
Kirkpatrick, S.\BBACOMMA\  \BBA\ Selman, B. \BBOP1994\BBCP.
\newblock \BBOQ Critical behavior in the satisfiability of random {B}oolean
  expressions\BBCQ\
\newblock {\Bem Science}, {\Bem 264}, 1297--1301.

\bibitem[\protect\BCAY{Kraj'icek}{Kraj'icek}{1997}]{krajicek-pb-clique}
Kraj'icek, J. \BBOP1997\BBCP.
\newblock \BBOQ Interpolation theorems, lower bounds for proof systems, and
  independence results for bounded arithmetic\BBCQ\
\newblock {\Bem J. Symb. Logic}, {\Bem 62\/}(2), 457--486.

\bibitem[\protect\BCAY{Krishnamurthy}{Krishnamurthy}{1985}]{krish:symmetry}
Krishnamurthy, B. \BBOP1985\BBCP.
\newblock \BBOQ Short proofs for tricky formulas\BBCQ\
\newblock {\Bem Acta Informatica}, {\Bem 22\/}(3), 253--275.

\bibitem[\protect\BCAY{Leone, Pfeifer,\ \BBA\ et~al.}{Leone
  et~al.}{2002}]{dlv02}
Leone, N., Pfeifer, G., \BBA\ et~al. \BBOP2002\BBCP.
\newblock \BBOQ The {DLV} system for knowledge representation and
  reasoning\BBCQ\
\newblock \BTR\ 1843-02-14, Technical University of Vienna.

\bibitem[\protect\BCAY{Li}{Li}{2000}]{Li:mod2}
Li, C.~M. \BBOP2000\BBCP.
\newblock \BBOQ Integrating equivalency reasoning into {D}avis-{P}utnam
  procedure\BBCQ\
\newblock In {\Bem Proceedings of the Seventeenth National Conference on
  Artificial Intelligence}, \BPGS\ 291--296.

\bibitem[\protect\BCAY{Li\ \BBA\ Anbulagan}{Li\ \BBA\
  Anbulagan}{1997}]{li:unitprop}
Li, C.~M.\BBACOMMA\  \BBA\ Anbulagan \BBOP1997\BBCP.
\newblock \BBOQ Heuristics based on unit propagation for satisfiability
  problems\BBCQ\
\newblock In {\Bem Proceedings of the Fifteenth International Joint Conference
  on Artificial Intelligence}, \BPGS\ 366--371.

\bibitem[\protect\BCAY{Luks\ \BBA\ Roy}{Luks\ \BBA\ Roy}{2002}]{Luks:symmetry}
Luks, E.\BBACOMMA\  \BBA\ Roy, A. \BBOP2002\BBCP.
\newblock \BBOQ Symmetry breaking in constraint satisfaction\BBCQ\
\newblock In {\Bem Intl. Conf. of Artificial Intelligence and Mathematics}, Ft.
  Lauderdale, Florida.

\bibitem[\protect\BCAY{Marek\ \BBA\ Truszczynski}{Marek\ \BBA\
  Truszczynski}{1999}]{Marek:stable}
Marek, V.~W.\BBACOMMA\  \BBA\ Truszczynski, M. \BBOP1999\BBCP.
\newblock \BBOQ Stable models and an alternative logic programming
  paradigm\BBCQ.

\bibitem[\protect\BCAY{McCarthy}{McCarthy}{1977}]{McCarthy77}
McCarthy, J. \BBOP1977\BBCP.
\newblock \BBOQ Epistemological problems of artificial intelligence\BBCQ\
\newblock In {\Bem Proceedings of the Fifth International Joint Conference on
  Artificial Intelligence}, \BPGS\ 1038--1044, Cambridge, MA.

\bibitem[\protect\BCAY{McCune\ \BBA\ Wos}{McCune\ \BBA\ Wos}{1997}]{Otter}
McCune, W.\BBACOMMA\  \BBA\ Wos, L. \BBOP1997\BBCP.
\newblock \BBOQ Otter - the {CADE}-13 competition incarnations\BBCQ\
\newblock {\Bem Journal of Automated Reasoning}, {\Bem 18\/}(2), 211--220.

\bibitem[\protect\BCAY{Mitchell}{Mitchell}{1998}]{Mitchell:hard}
Mitchell, D.~G. \BBOP1998\BBCP.
\newblock \BBOQ Hard problems for {CSP} algorithms\BBCQ\
\newblock In {\Bem Proceedings of the Fifteenth National Conference on
  Artificial Intelligence}, \BPGS\ 398--405.

\bibitem[\protect\BCAY{Moskewicz, Madigan, Zhao, Zhang,\ \BBA\ Malik}{Moskewicz
  et~al.}{2001}]{zchaff}
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., \BBA\ Malik, S.
  \BBOP2001\BBCP.
\newblock \BBOQ Chaff: {E}ngineering an efficient {SAT} solver\BBCQ\
\newblock In {\Bem 39th Design Automation Conference}.

\bibitem[\protect\BCAY{Nemhauser\ \BBA\ Wolsey}{Nemhauser\ \BBA\
  Wolsey}{1988}]{OR:cut}
Nemhauser, G.\BBACOMMA\  \BBA\ Wolsey, L. \BBOP1988\BBCP.
\newblock {\Bem Integer and Combinatorial Optimization}.
\newblock Wiley, New York.

\bibitem[\protect\BCAY{Niemel\"a}{Niemel\"a}{1999}]{Niemela:ASP}
Niemel\"a, I. \BBOP1999\BBCP.
\newblock \BBOQ Logic programs with stable model semantics as a constraint
  programming paradigm\BBCQ\
\newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem 25},
  241--273.

\bibitem[\protect\BCAY{Papadimitriou}{Papadimitriou}{1994}]{Papadimitriou:smal%
lok}
Papadimitriou, C. \BBOP1994\BBCP.
\newblock {\Bem Computational Complexity}.
\newblock Addison-Wesley.

\bibitem[\protect\BCAY{Parkes}{Parkes}{1999}]{Parkes:thesis}
Parkes, A.~J. \BBOP1999\BBCP.
\newblock {\Bem Lifted Search Engines for Satisfiability}.
\newblock Ph.D.\ thesis, University of Oregon.
\newblock Available from {\sf http://www.cirl.uoregon.edu/parkes}.

\bibitem[\protect\BCAY{Pearce}{Pearce}{1997}]{Pearce:LHT}
Pearce, D. \BBOP1997\BBCP.
\newblock \BBOQ A new logical characterization of stable models and answer
  sets\BBCQ\
\newblock In Dix, J., Pereira, L., \BBA\ Przymusinski, T.\BEDS, {\Bem
  Non-monotonic Extensions of Logic Programming}, \lowercase{\BVOL}\ 1216 of
  {\Bem Lecture Notes in Artificial Intelligence}, \BPGS\ 57--70.

\bibitem[\protect\BCAY{Pitassi}{Pitassi}{2002}]{Pitassi:complexity}
Pitassi, T. \BBOP2002\BBCP.
\newblock \BBOQ Propositional proof complexity lecture notes\BBCQ\
\newblock {\sf
  www.cs.toronto.edu/\~{}toni/Courses/Proofcomplexity/Lectures/Lecture1/lectur%
e1.ps} (other lectures titled similarly).

\bibitem[\protect\BCAY{Prestwich}{Prestwich}{2002}]{Prestwich:pb}
Prestwich, S. \BBOP2002\BBCP.
\newblock \BBOQ Randomised backtracking for linear pseudo-{B}oolean constraint
  problems\BBCQ\
\newblock In {\Bem Proceedings of the 4th International Workshop on Integration
  of AI and OR Techniques in Constraint Programming for Combinatorial
  Optimisation Problems (CPAIOR-02)}, \BPGS\ 7--20.

\bibitem[\protect\BCAY{Pretolani}{Pretolani}{1993}]{Pretolani:branching}
Pretolani, D. \BBOP1993\BBCP.
\newblock {\Bem Satisfiability and hypergraphs}.
\newblock Ph.D.\ thesis, Universita di Pisa.

\bibitem[\protect\BCAY{Pudlak}{Pudlak}{1997}]{clique}
Pudlak, P. \BBOP1997\BBCP.
\newblock \BBOQ Lower bounds for resolution and cutting planes proofs and
  monotone computations\BBCQ\
\newblock {\Bem J. Symbolic Logic}, {\Bem 62\/}(3), 981--998.

\bibitem[\protect\BCAY{Puget}{Puget}{1993}]{Puget:symmetry}
Puget, J.-F. \BBOP1993\BBCP.
\newblock \BBOQ On the satisfiability of symmetrical constrained satisfaction
  problems\BBCQ\
\newblock In {\Bem In J. Komorowski and Z.W. Ras, editors, Proceedings of
  ISMIS'93, pages 350--361. Springer-Verlag, 1993. Lecture Notes in Artificial
  Intelligence 689.}

\bibitem[\protect\BCAY{Reiter}{Reiter}{1978}]{Reiter:cwa}
Reiter, R. \BBOP1978\BBCP.
\newblock \BBOQ On closed world data bases\BBCQ\
\newblock In Gallaire, H.\BBACOMMA\  \BBA\ Minker, J.\BEDS, {\Bem Logic and
  Data Bases}, \BPGS\ 119--140. Plenum, New York.

\bibitem[\protect\BCAY{Savelsbergh}{Savelsbergh}{1994}]{Savelsbergh:preprocess}
Savelsbergh, M. W.~P. \BBOP1994\BBCP.
\newblock \BBOQ Preprocessing and probing for mixed integer programming
  problems\BBCQ\
\newblock {\Bem {ORSA} Journal on Computing}, {\Bem 6}, 445--454.

\bibitem[\protect\BCAY{Schaefer}{Schaefer}{1978}]{Schaefer:complexity}
Schaefer, T.~J. \BBOP1978\BBCP.
\newblock \BBOQ The complexity of satisfiability problems\BBCQ\
\newblock In {\Bem Proceedings of the Tenth Annual ACM Symposium on the Theory
  of Computing}, \BPGS\ 216--226.

\bibitem[\protect\BCAY{Selman, Kautz,\ \BBA\ Cohen}{Selman
  et~al.}{1993}]{Selman:wsat}
Selman, B., Kautz, H.~A., \BBA\ Cohen, B. \BBOP1993\BBCP.
\newblock \BBOQ Local search strategies for satisfiability testing\BBCQ\
\newblock In {\Bem Proceedings 1993 {DIMACS} Workshop on Maximum Clique, Graph
  Coloring, and Satisfiability}.

\bibitem[\protect\BCAY{Simons}{Simons}{2000}]{Simons:stable}
Simons, P. \BBOP2000\BBCP.
\newblock \BBOQ Extending and implementing the stable model semantics\BBCQ.
\newblock Research Report 58, Helsinki University of Technology, Helsinki,
  Finland.

\bibitem[\protect\BCAY{Stallman\ \BBA\ Sussman}{Stallman\ \BBA\
  Sussman}{1977}]{Sussman:ddb}
Stallman, R.~M.\BBACOMMA\  \BBA\ Sussman, G.~J. \BBOP1977\BBCP.
\newblock \BBOQ Forward reasoning and dependency-directed backtracking in a
  system for computer-aided circuit analysis\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 9}, 135--196.

\bibitem[\protect\BCAY{Szeider}{Szeider}{2003}]{Szeider:symmetry}
Szeider, S. \BBOP2003\BBCP.
\newblock \BBOQ The complexity of resolution with generalized symmetry
  rules\BBCQ\
\newblock In Alt, H.\BBACOMMA\  \BBA\ Habib, M.\BEDS, {\Bem Proceedings of
  STACS03, volume 2607 of Springer Lecture Notes in Computer Science}, \BPGS\
  475--486.

\bibitem[\protect\BCAY{Tseitin}{Tseitin}{1970}]{Tseitin:complexity}
Tseitin, G. \BBOP1970\BBCP.
\newblock \BBOQ On the complexity of derivation in propositional calculus\BBCQ\
\newblock In Slisenko, A.\BED, {\Bem Studies in Constructive Mathematics and
  Mathematical Logic, {P}art 2}, \BPGS\ 466--483. Consultants Bureau.

\bibitem[\protect\BCAY{Urquhart}{Urquhart}{1995}]{urquhart:complexity}
Urquhart, A. \BBOP1995\BBCP.
\newblock \BBOQ The complexity of propositional proofs\BBCQ\
\newblock {\Bem Bull. Symbolic Logic}, {\Bem 1\/}(4), 425--467.

\bibitem[\protect\BCAY{Velev\ \BBA\ Bryant}{Velev\ \BBA\
  Bryant}{2001}]{Velev:verify}
Velev, M.~N.\BBACOMMA\  \BBA\ Bryant, R.~E. \BBOP2001\BBCP.
\newblock \BBOQ Effective use of boolean satisfiability procedures in the
  formal verification of superscalar and {VLIW}\BBCQ\
\newblock In {\Bem Proceedings of the 38th Conference on Design Automation
  Conference 2001}, \BPGS\ 226--231, New York, NY, USA. ACM Press.

\bibitem[\protect\BCAY{Walser}{Walser}{1997}]{Walser:WSATPB}
Walser, J.~P. \BBOP1997\BBCP.
\newblock \BBOQ Solving linear pseudo-{B}oolean constraint problems with local
  search\BBCQ\
\newblock In {\Bem Proceedings of the Fourteenth National Conference on
  Artificial Intelligence}, \BPGS\ 269--274.

\bibitem[\protect\BCAY{Zhang\ \BBA\ Stickel}{Zhang\ \BBA\
  Stickel}{2000}]{Zhang:watch}
Zhang, H.\BBACOMMA\  \BBA\ Stickel, M.~E. \BBOP2000\BBCP.
\newblock \BBOQ Implementing the {D}avis-{P}utnam method\BBCQ\
\newblock {\Bem Journal of Automated Reasoning}, {\Bem 24\/}(1/2), 277--296.

\end{thebibliography}
