next up previous
Next: About this document ... Up: Generalizing Boolean Satisfiability I: Previous: Acknowledgments


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.

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.

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

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.

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

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.

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

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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'icek, J. 1997.
Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
J. Symb. Logic, 62(2), 457-486.

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.

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.

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.

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ä, I. 1999.
Logic programs with stable model semantics as a constraint programming paradigm
Annals of Mathematics and Artificial Intelligence, 25, 241-273.

Papadimitriou, C. 1994.
Computational Complexity.

Parkes, A. J. 1999.
Lifted Search Engines for Satisfiability.
Ph.D. thesis, University of Oregon.
Available from

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.

Pitassi, T. 2002.
Propositional proof complexity lecture notes (other lectures titled similarly).

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.

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

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

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.

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

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

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.

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.

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.

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.

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.

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.

Matt Ginsberg 2004-02-19