Bibliography

Aloul, Ramani, Markov, SakallahAloul et al.2002

Aloul, F., Ramani, A., Markov, I., Sakallah, K. 2002.
PBS: A backtrack search pseudo-Boolean solver
In Symposium on the Theory and Applications of Satisfiability Testing.

BabaiBabai1995

Babai, L. 1995.
Automorphism groups, isomorphism, reconstruction
In Lovász, L., Graham, R., Grötschel, M., Handbook for Combinatorics, 27, 1447-1540. North-Holland-Elsevier.

BakerBaker1994

Baker, A. B. 1994.
The hazards of fancy backtracking
In Proceedings of the Twelfth National Conference on Artificial Intelligence.

BarthBarth1995

Barth, P. 1995.
A Davis-Putnam based enumeration algorithm for linear pseudo-boolean optimization
MPI-I-95-2-003, Max Planck Institut für Informatik, Saarbrücken, Germany.

BarthBarth1996

Barth, P. 1996.
Logic-Based 0-1 Constraint Programming, 5 of Operations Research/Computer Science Interfaces Series.
Kluwer.

BaumgartnerBaumgartner2000

Baumgartner, P. 2000.
FDPLL - A First-Order Davis-Putnam-Logeman-Loveland Procedure
In McAllester, D., CADE-17 - The 17th International Conference on Automated Deduction, 1831, 200-219. Springer.

Bayardo MirankerBayardo Miranker1996

Bayardo, R. J. Miranker, D. P. 1996.
A complexity analysis of space-bounded learning algorithms for the constraint satisfaction problem
In Proceedings of the Thirteenth National Conference on Artificial Intelligence, 298-304.

Bayardo SchragBayardo Schrag1997

Bayardo, R. J. Schrag, R. C. 1997.
Using CSP look-back techniques to solve real-world SAT instances
In Proceedings of the Fourteenth National Conference on Artificial Intelligence, 203-208.

Beame PitassiBeame Pitassi2001

Beame, P. Pitassi, T. 2001.
Propositional proof complexity: Past, present and future
In Paun, G., Rozenberg, G., Salomaa, A., Current Trends in Theoretical Computer Science, Entering the 21th Century, 42-70. World Scientific.

Benhamou, Sais, SiegelBenhamou et al.1994

Benhamou, B., Sais, L., Siegel, P. 1994.
Two proof procedures for a cardinality based language in propositional calculus
In Proceedings of STACS94, volume 775 de Lecture Notes in Computer Science.

Biere, Clarke, Raimi, ZhuBiere et al.1999

Biere, A., Clarke, E., Raimi, R., Zhu, Y. 1999.
Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs
Lecture Notes in Computer Science, 1633.

Bonet, Pitassi, RazBonet et al.1997

Bonet, M. L., Pitassi, T., Raz, R. 1997.
Lower bounds for cutting planes proofs with small coefficients
Journal of Symbolic Logic, 62(3), 708-728.

Brown, Finkelstein, Paul Walton PurdomBrown et al.1988

Brown, C. A., Finkelstein, L., Paul Walton Purdom, J. 1988.
Backtrack searching in the presence of symmetry
In Mora, T., Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, 6th Int'l. Conf., 99-110. Springer-Verlag.

BryantBryant1986

Bryant, R. E. 1986.
Graph-based algorithms for Boolean function manipulation
IEEE Transactions on Computers, C-35(8), 677-691.

BryantBryant1992

Bryant, R. E. 1992.
Symbolic Boolean manipulation with ordered binary-decision diagrams
ACM Computing Surveys, 24(3), 293-318.

BuchbergerBuchberger1965

Buchberger, B. 1965.
Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einum nulldimensionalen Polynomideal.
Ph.D. thesis, University of Innsbruck, Innsbruck.

BuchbergerBuchberger1985

Buchberger, B. 1985.
Gröbner bases: An algorithmic method in polynomial ideal theory
In Bose, N., Multidimensional Systems Theory. D. Reidel, Dordrecht, Holland.

Cadoli, Schaerf, Giovanardi, GiovanardiCadoli et al.2002

Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M. 2002.
An algorithm to evaluate quantified boolean formulae and its experimental evaluation
Journal of Automated Reasoning, 28(2), 101-142.

Chai KuehlmannChai Kuehlmann2003

Chai, D. Kuehlmann, A. 2003.
A fast pseudo-Boolean constraint solver
In Proceedings of the 40th Design Automation Conference, 830-835.

Chandru HookerChandru Hooker1999

Chandru, V. Hooker, J. N. 1999.
Optimization Mehtods for Logical Inference.
Wiley-Interscience.

Clegg, Edmonds, ImpagliazzoClegg et al.1996

Clegg, M., Edmonds, J., Impagliazzo, R. 1996.
Using the Groebner basis algorithm to find proofs of unsatisfiability
In Proceedings of the Twenty-Eighth Annual ACM Symp. on Theory of Computing, 174-183.

Coarfa, Demopoulos, San Miguel Aguirre, Subramanian, VardiCoarfa et al.2000

Coarfa, C., Demopoulos, D. D., San Miguel Aguirre, A., Subramanian, D., Vardi, M. 2000.
Random 3-SAT: The plot thickens
In Proceedings of the International Conference on Constraint Programming.

CookCook1971

Cook, S. A. 1971.
The complexity of theorem-proving procedures
In Proceedings of the 3rd Annual ACM Symposium on the Theory of Computing, 151-158.

Cook, Coullard, TuranCook et al.1987

Cook, W., Coullard, C., Turan, G. 1987.
On the complexity of cutting-plane proofs
Discrete Applied Mathematics, 18, 25-38.

Copty, Fix, Giunchiglia, Kamhi, Tacchella, VardiCopty et al.2001

Copty, F., Fix, L., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M. 2001.
Benefits of bounded model checking in an industrial setting
In 13th Conference on Computer Aided Verification, CAV'01, Paris, France.

CrawfordCrawford1992

Crawford, J. M. 1992.
A theoretical analysis of reasoning by symmetry in first-order logic (extended abstract)
In AAAI Workshop on Tractable Reasoning.

Crawford AutonCrawford Auton1996

Crawford, J. M. Auton, L. D. 1996.
Experimental results on the crossover point in random 3SAT
Artificial Intelligence, 81, 31-57.

Crawford, Ginsberg, Luks, RoyCrawford et al.1996

Crawford, J. M., Ginsberg, M. L., Luks, E., Roy, A. 1996.
Symmetry breaking predicates for search problems
In Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, Boston, MA.

Davis PutnamDavis Putnam1960

Davis, M. Putnam, H. 1960.
A computing procedure for quantification theory
J. Assoc. Comput. Mach., 7, 201-215.

Davis, Logemann, LovelandDavis et al.1962

Davis, M., Logemann, G., Loveland, D. 1962.
A machine program for theorem-proving
Communications of the ACM, 5(7), 394-397.

DechterDechter1990

Dechter, R. 1990.
Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition
Artificial Intelligence, 41, 273-312.

Dixon GinsbergDixon Ginsberg2000

Dixon, H. E. Ginsberg, M. L. 2000.
Combining satisfiability techniques from AI and OR
Knowledge Engrg. Rev., 15, 31-45.

Dixon GinsbergDixon Ginsberg2002

Dixon, H. E. Ginsberg, M. L. 2002.
Inference methods for a pseudo-Boolean satisfiability solver
In Proceedings of the Eighteenth National Conference on Artificial Intelligence.

Dixon, Ginsberg, Hofer, Luks, ParkesDixon et al.2003a

Dixon, H. E., Ginsberg, M. L., Hofer, D., Luks, E. M., Parkes, A. J. 2003a.
Generalizing Boolean satisfiability III: Implementation
, Computational Intelligence Research Laboratory, Eugene, Oregon.

Dixon, Ginsberg, Luks, ParkesDixon et al.2003b

Dixon, H. E., Ginsberg, M. L., Luks, E. M., Parkes, A. J. 2003b.
Generalizing Boolean satisfiability II: Theory
, Computational Intelligence Research Laboratory, Eugene, Oregon.

Dubois, Andre, Boufkhad, CarlierDubois et al.1993

Dubois, O., Andre, P., Boufkhad, Y., Carlier, J. 1993.
SAT versus UNSAT
In Second DIMACS Challenge: Cliques, Colorings and Satisfiability, Rutgers University, NJ.

Dubois DequenDubois Dequen2001

Dubois, O. Dequen, G. 2001.
A backbone-search heuristic for efficient solving of hard 3-SAT formulae
In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 248-253.

East TruszczynskiEast Truszczynski2001

East, D. Truszczynski, M. 2001.
Propositional satisfiability in answer-set programming
Lecture Notes in Computer Science, 2174.

East TruszczynskiEast Truszczynski2002

East, D. Truszczynski, M. 2002.
Propositional satisfiability in declarative programming
Extended version of papers that appeared in Proceedings of AAAI-2000 and Proceedings of KI-2001. http://xxx.lanl.gov/abs/cs.LO/0211033.

FreemanFreeman1995

Freeman, J. W. 1995.
Improvements to propositional satisfiability search algorithms.
Ph.D. thesis, University of Pennsylvania, PA.

Frost DechterFrost Dechter1994

Frost, D. Dechter, R. 1994.
Dead-end driven learning
In Proceedings of the Twelfth National Conference on Artificial Intelligence, 294-300.

Galperin WigdersonGalperin Wigderson1983

Galperin, H. Wigderson, A. 1983.
Succinct representation of graphs
Information and Control, 56, 183-198.

Garey JohnsonGarey Johnson1979

Garey, M. Johnson, D. 1979.
Computers and Intractability.
W.H. Freeman and Co., New York.

GaschnigGaschnig1979

Gaschnig, J. 1979.
Performance measurement and analysis of certain search algorithms
CMU-CS-79-124, Carnegie-Mellon University.

Gelfond LifschitzGelfond Lifschitz1988

Gelfond, M. Lifschitz, V. 1988.
The stable semantics for logic programs
In Proceedings of the 5th International Conference on Logic Programming, 1070-1080. MIT Press.

GinsbergGinsberg1993

Ginsberg, M. L. 1993.
Dynamic backtracking
Journal of Artificial Intelligence Research, 1, 25-46.

Ginsberg GeddisGinsberg Geddis1991

Ginsberg, M. L. Geddis, D. F. 1991.
Is there any need for domain-dependent control information?
In Proceedings of the Ninth National Conference on Artificial Intelligence.

Ginsberg ParkesGinsberg Parkes2000

Ginsberg, M. L. Parkes, A. J. 2000.
Search, subsearch and QPROP
In Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning, Breckenridge, Colorado.

Goldberg NovikovGoldberg Novikov2002

Goldberg, E. Novikov, Y. 2002.
Berkmin: A fast and robust SAT solver
In Design Automation and Test in Europe (DATE), 142-149.

Guignard SpielbergGuignard Spielberg1981

Guignard, M. Spielberg, K. 1981.
Logical reduction methods in zero-one programming
Operations Research, 29.

HakenHaken1985

Haken, A. 1985.
The intractability of resolution
Theoretical Computer Science, 39, 297-308.

HakenHaken1995

Haken, A. 1995.
Counting bottlenecks to show monotone $P\neq NP$
In Proceedings 36th Annual IEEE Symp. on Foundations of Computer Science (FOCS-95), 36-40, Milwaukee, MN. IEEE.

HookerHooker1988

Hooker, J. N. 1988.
Generalized resolution and cutting planes
Annals of Operations Research, 12, 217-239.

Hooker VinayHooker Vinay1995

Hooker, J. N. Vinay, V. 1995.
Branching rules for satisfiability
J. Automated Reasoning, 15, 359-383.

Jeroslow WangJeroslow Wang1990

Jeroslow, R. Wang, J. 1990.
Solving the propositional satisfiability problem
Annals of Mathematics and Artificial Intelligence, 1, 167-187.

Joslin RoyJoslin Roy1997

Joslin, D. Roy, A. 1997.
Exploiting symmetry in lifted CSPs
In Proceedings of the Fourteenth National Conference on Artificial Intelligence, 197-202.

Kautz SelmanKautz Selman1998

Kautz, H. Selman, B. 1998.
BLACKBOX: A new approach to the application of theorem proving to problem solving
In Artificial Intelligence Planning Systems: Proceedings of the Fourth International Conference. AAAI Press.

Kautz SelmanKautz Selman1992

Kautz, H. A. Selman, B. 1992.
Planning as satisfiability
In Proceedings of the Tenth European Conference on Artificial Intelligence (ECAI'92), 359-363.

Kirkpatrick SelmanKirkpatrick Selman1994

Kirkpatrick, S. Selman, B. 1994.
Critical behavior in the satisfiability of random Boolean expressions
Science, 264, 1297-1301.

Kraj'icekKraj'icek1997

Kraj'icek, J. 1997.
Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
J. Symb. Logic, 62(2), 457-486.

KrishnamurthyKrishnamurthy1985

Krishnamurthy, B. 1985.
Short proofs for tricky formulas
Acta Informatica, 22(3), 253-275.

Leone, Pfeifer, et al.Leone et al.2002

Leone, N., Pfeifer, G., et al. 2002.
The DLV system for knowledge representation and reasoning
1843-02-14, Technical University of Vienna.

LiLi2000

Li, C. M. 2000.
Integrating equivalency reasoning into Davis-Putnam procedure
In Proceedings of the Seventeenth National Conference on Artificial Intelligence, 291-296.

Li AnbulaganLi Anbulagan1997

Li, C. M. Anbulagan 1997.
Heuristics based on unit propagation for satisfiability problems
In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 366-371.

Luks RoyLuks Roy2002

Luks, E. Roy, A. 2002.
Symmetry breaking in constraint satisfaction
In Intl. Conf. of Artificial Intelligence and Mathematics, Ft. Lauderdale, Florida.

Marek TruszczynskiMarek Truszczynski1999

Marek, V. W. Truszczynski, M. 1999.
Stable models and an alternative logic programming paradigm.

McCarthyMcCarthy1977

McCarthy, J. 1977.
Epistemological problems of artificial intelligence
In Proceedings of the Fifth International Joint Conference on Artificial Intelligence, 1038-1044, Cambridge, MA.

McCune WosMcCune Wos1997

McCune, W. Wos, L. 1997.
Otter - the CADE-13 competition incarnations
Journal of Automated Reasoning, 18(2), 211-220.

MitchellMitchell1998

Mitchell, D. G. 1998.
Hard problems for CSP algorithms
In Proceedings of the Fifteenth National Conference on Artificial Intelligence, 398-405.

Moskewicz, Madigan, Zhao, Zhang, MalikMoskewicz et al.2001

Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S. 2001.
Chaff: Engineering an efficient SAT solver
In 39th Design Automation Conference.

Nemhauser WolseyNemhauser Wolsey1988

Nemhauser, G. Wolsey, L. 1988.
Integer and Combinatorial Optimization.
Wiley, New York.

NiemeläNiemelä1999

Niemelä, I. 1999.
Logic programs with stable model semantics as a constraint programming paradigm
Annals of Mathematics and Artificial Intelligence, 25, 241-273.

PapadimitriouPapadimitriou1994

Papadimitriou, C. 1994.
Computational Complexity.
Addison-Wesley.

ParkesParkes1999

Parkes, A. J. 1999.
Lifted Search Engines for Satisfiability.
Ph.D. thesis, University of Oregon.
Available from http://www.cirl.uoregon.edu/parkes.

PearcePearce1997

Pearce, D. 1997.
A new logical characterization of stable models and answer sets
In Dix, J., Pereira, L., Przymusinski, T., Non-monotonic Extensions of Logic Programming, 1216 of Lecture Notes in Artificial Intelligence, 57-70.

PitassiPitassi2002

Pitassi, T. 2002.
Propositional proof complexity lecture notes
www.cs.toronto.edu/~toni/Courses/Proofcomplexity/Lectures/Lecture1/lecture1.ps (other lectures titled similarly).

PrestwichPrestwich2002

Prestwich, S. 2002.
Randomised backtracking for linear pseudo-Boolean constraint problems
In Proceedings of the 4th International Workshop on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimisation Problems (CPAIOR-02), 7-20.

PretolaniPretolani1993

Pretolani, D. 1993.
Satisfiability and hypergraphs.
Ph.D. thesis, Universita di Pisa.

PudlakPudlak1997

Pudlak, P. 1997.
Lower bounds for resolution and cutting planes proofs and monotone computations
J. Symbolic Logic, 62(3), 981-998.

PugetPuget1993

Puget, J.-F. 1993.
On the satisfiability of symmetrical constrained satisfaction problems
In In J. Komorowski and Z.W. Ras, editors, Proceedings of ISMIS'93, pages 350-361. Springer-Verlag, 1993. Lecture Notes in Artificial Intelligence 689.

ReiterReiter1978

Reiter, R. 1978.
On closed world data bases
In Gallaire, H. Minker, J., Logic and Data Bases, 119-140. Plenum, New York.

SavelsberghSavelsbergh1994

Savelsbergh, M. W. P. 1994.
Preprocessing and probing for mixed integer programming problems
ORSA Journal on Computing, 6, 445-454.

SchaeferSchaefer1978

Schaefer, T. J. 1978.
The complexity of satisfiability problems
In Proceedings of the Tenth Annual ACM Symposium on the Theory of Computing, 216-226.

Selman, Kautz, CohenSelman et al.1993

Selman, B., Kautz, H. A., Cohen, B. 1993.
Local search strategies for satisfiability testing
In Proceedings 1993 DIMACS Workshop on Maximum Clique, Graph Coloring, and Satisfiability.

SimonsSimons2000

Simons, P. 2000.
Extending and implementing the stable model semantics.
Research Report 58, Helsinki University of Technology, Helsinki, Finland.

Stallman SussmanStallman Sussman1977

Stallman, R. M. Sussman, G. J. 1977.
Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
Artificial Intelligence, 9, 135-196.

SzeiderSzeider2003

Szeider, S. 2003.
The complexity of resolution with generalized symmetry rules
In Alt, H. Habib, M., Proceedings of STACS03, volume 2607 of Springer Lecture Notes in Computer Science, 475-486.

TseitinTseitin1970

Tseitin, G. 1970.
On the complexity of derivation in propositional calculus
In Slisenko, A., Studies in Constructive Mathematics and Mathematical Logic, Part 2, 466-483. Consultants Bureau.

UrquhartUrquhart1995

Urquhart, A. 1995.
The complexity of propositional proofs
Bull. Symbolic Logic, 1(4), 425-467.

Velev BryantVelev Bryant2001

Velev, M. N. Bryant, R. E. 2001.
Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW
In Proceedings of the 38th Conference on Design Automation Conference 2001, 226-231, New York, NY, USA. ACM Press.

WalserWalser1997

Walser, J. P. 1997.
Solving linear pseudo-Boolean constraint problems with local search
In Proceedings of the Fourteenth National Conference on Artificial Intelligence, 269-274.

Zhang StickelZhang Stickel2000

Zhang, H. Stickel, M. E. 2000.
Implementing the Davis-Putnam method
Journal of Automated Reasoning, 24(1/2), 277-296.