Contents of Bibliography

ccisdefined journalfont

Bibliography

D. Achlioptas, P. Beame, and M. Molloy.: A sharp threshold in proof complexity.
In Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing, pages 337-346, Crete, Greece, July 2001.
M. Alekhnovich, J. Johannsen, T. Pitassi, and A. Urquhart.: An exponential separation between regular and general resolution.
In Proceedings of the Thirty-Fourth Annual ACM Symposium on Theory of Computing, pages 448-456, Montréal, Canada, May 2002.
F. A. Aloul, A. Ramani, I. L. Markov, and K. A. Sakallah.: Solving difficult SAT instances in the presence of symmetry.
In Proceedings of the 39th Design Automation Conference, pages 731-736, New Orleans, LA, June 2002. ACM.
E. Amir and S. A. McIlraith.: Partition-based logical reasoning.
In Proceedings of the 7th International Conference on Principles of Knowledge Representation and Reasoning, pages 389-400, Breckenridge, CO, Apr. 2000.
A. Atserias and M. L. Bonet.: On the automatizability of resolution and related propositional proof systems.
In CSL '02: 16th Workshop on Computer Science Logic, volume 2471 of Lecture Notes in Computer Science, pages 569-583, Edinburgh, Scotland, Sept. 2002. Springer.
A. Aziz, S. Tasiran, and R. K. Brayton.: BDD variable orderings for interacting finite state machines.
In Proceedings of the 31th Design Automation Conference, pages 283-288, San Diego, CA, June 1994. ACM.
L. Baptista and J. P. M. Silva.: Using randomization and learning to solve hard real-world instances of satisfiability.
In 6th Principles and Practice of Constraint Programming, pages 489-494, 2000.
URL citeseer.nj.nec.com/baptista00using.html.
R. J. Bayardo Jr. and R. C. Schrag.: Using CST look-back techniques to solve real-world SAT instances.
In Proceedings, AAAI-97: 14th National Conference on Artificial Intelligence, pages 203-208, Providence, Rhode Island, July 1997.
P. Beame, R. Impagliazzo, T. Pitassi, and N. Segerlind.: Memoization and DPLL: Formula caching proof systems.
In Proceedings 18th Annual IEEE Conference on Computational Complexity, pages 225-236, Aarhus, Denmark, July 2003a.
P. Beame, H. Kautz, and A. Sabharwal.: Understanding the power of clause learning.
In Proceedings of the 18th International Joint Conference on Artificial Intelligence, pages 1194-1201, Acapulco, Mexico, Aug. 2003b.
E. Ben-Sasson, R. Impagliazzo, and A. Wigderson.: Near-optimal separation of treelike and general resolution.
Technical Report TR00-005, Electronic Colloquium in Computation Complexity, http://www.eccc.uni-trier.de/eccc/, 2000.
To appear in Combinatorica.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu.: Symbolic model checking using SAT procedures instead of BDDs.
In Proceedings of the 36th Design Automation Conference, pages 317-320, New Orleans, LA, June 1999a. ACM.
A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu.: Symbolic model checking without BDDs.
In 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 193-207, Amsterdam, the Netherlands, Mar. 1999b.
M. L. Bonet, J. L. Esteban, N. Galesi, and J. Johansen.: On the relative complexity of resolution refinements and cutting planes proof systems.
SIAM Journal on Computing, 30 (5): 1462-1484, 2000.
M. L. Bonet and N. Galesi.: Optimality of size-width tradeoffs for resolution.
Computational Complexity, 10 (4): 261-276, 2001.
R. I. Brafman.: A simplifier for propositional formulas with many binary clauses.
In Proceedings of the 17th International Joint Conference on Artificial Intelligence, pages 515-522, Seattle, WA, Aug. 2001.
J. Buresh-Oppenheim and T. Pitassi.: The complexity of resolution refinements.
In 18th Annual IEEE Symposium on Logic in Computer Science, pages 138-147, Ottawa, Canada, June 2003.
S. A. Cook and R. A. Reckhow.: The relative efficiency of propositional proof systems.
Journal of Symbolic Logic, 44 (1): 36-50, 1977.
M. Davis, G. Logemann, and D. Loveland.: A machine program for theorem proving.
Communications of the ACM, 5: 394-397, 1962.
M. Davis and H. Putnam.: A computing procedure for quantification theory.
Communications of the ACM, 7: 201-215, 1960.
R. Davis.: Diagnostic reasoning based on structure and behavior.
Artificial Intelligence, 24: 347-410, 1984.
J. de Kleer and B. C. Williams.: Diagnosing multiple faults.
Artificial Intelligence, 32 (1): 97-130, 1987.
J. L. Esteban, N. Galesi, and J. Messner.: On the complexity of resolution with bounded conjunctions.
In Automata, Languages, and Programming: 29th International Colloquium, volume 2380 of Lecture Notes in Computer Science, pages 220-231, Malaga, Spain, July 2002. Springer-Verlag.
R. Genesereth.: The use of design descriptions in automated diagnosis.
Artificial Intelligence, 24: 411-436, 1984.
E. Giunchiglia, M. Maratea, and A. Tacchella.: Dependent and independent variables in propositional satisfiability.
In Proceedings of the 8th European Conference on Logics in Artificial Intelligence (JELIA), volume 2424 of Lecture Notes in Computer Science, pages 296-307, Cosenza, Italy, Sept. 2002. Springer-Verlag.
C. P. Gomes, B. Selman, and H. Kautz.: Boosting combinatorial search through randomization.
In Proceedings, AAAI-98: 15th National Conference on Artificial Intelligence, pages 431-437, Madison, WI, 1998a.
URL citeseer.nj.nec.com/gomes98boosting.html.
C. P. Gomes, B. Selman, K. McAloon, and C. Tretkoff.: Randomization in backtrack search: Exploiting heavy-tailed profiles for solving hard scheduling problems.
In Proceedings of the 4th International Conference on Artificial Intelligence Planning Systems, Pittsburgh, PA, June 1998b.
A. Haken.: The intractability of resolution.
Theoretical Computer Science, 39: 297-305, 1985.
J. E. Harlow and F. Brglez.: Design of experiments in BDD variable ordering: Lessons learned.
In Proceedings of the International Conference on Computer Aided Design, pages 646-652, San Jose, CA, Nov. 1998. IEEE/ACM.
D. S. Johnson and M. A. Trick, editors.: Cliques, Coloring and Satisfiability: Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science.
AMS, 1996.
H. A. Kautz and B. Selman.: Planning as satisfiability.
In Proceedings of the 10th European Conference on Artificial Intelligence, pages 359-363, Vienna, Austria, Aug. 1992.
H. A. Kautz and B. Selman.: Pushing the envelope: Planning, propositional logic, and stochastic search.
In Proceedings, AAAI-96: 13th National Conference on Artificial Intelligence, pages 1194-1201, Portland, OR, Aug. 1996.
H. Konuk and T. Larrabee.: Explorations of sequential ATPG using boolean satisfiability.
In 11th VLSI Test Symposium, pages 85-90, 1993.
J. Krají $\textrm{\v{c\/}}\kern.05em$ ek.: On the weak pigeonhole principle.
Fundamenta Mathematicae, 170 (1-3): 123-140, 2001.
B. Krishnamurthy.: Short proofs for tricky formulas.
Acta Informatica, 22: 253-274, 1985.
C. M. Li and Anbulagan.: Heuristics based on unit propagation for satisfiability problems.
In Proceedings of the 15th International Joint Conference on Artificial Intelligence, pages 366-371, Nagoya, Japan, Aug. 1997.
URL citeseer.nj.nec.com/li97heuristics.html.
J. Marques-Silva.: An overview of backtrack search satisfiability algorithms.
In 5th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, Jan. 1998.
J. P. Marques-Silva and K. A. Sakallah.: GRASP - a new search algorithm for satisfiability.
In Proceedings of the International Conference on Computer Aided Design, pages 220-227, San Jose, CA, Nov. 1996. ACM/IEEE.
M. Mézard and R. Zecchina.: Random k-satisfiability problem: From an analytic solution to an efficient algorithm.
Physical Review E, 66: 056126, Nov. 2002.
M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik.: Chaff: Engineering an efficient SAT solver.
In Proceedings of the 38th Design Automation Conference, pages 530-535, Las Vegas, NV, June 2001. ACM.
R. Ostrowski, E. Grégoire, B. Mazure, and L. Sais.: Recovering and exploiting structural knowledge from cnf formulas.
In 8th Principles and Practice of Constraint Programming, volume 2470 of Lecture Notes in Computer Science, pages 185-199, Ithaca, NY, Sept. 2002. Springer-Verlag.
S. Reda, R. Drechsler, and A. Orailoglu.: On the relation between SAT and BDDs for equivalence checking.
In Proceedings of the International Symposium on Quality Electronic Design, pages 394-399, San Jose, CA, Mar. 2002.
A. Sabharwal, P. Beame, and H. Kautz.: Using problem structure for efficient clause learning.
In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, volume 2919 of Lecture Notes in Computer Science, pages 242-256, Portofino, Italy, May 2003. Springer-Verlag.
O. Shtrichman.: Tuning SAT checkers for bounded model checking.
In Proceedings of the 12th International Conference on Computer Aided Verification, pages 480-494, Chicago, IL, July 2000.
R. Stallman and G. J. Sussman.: Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis.
Artificial Intelligence, 9: 135-196, 1977.
M. Velev and R. Bryant.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and vliw microprocessors.
In Proceedings of the 38th Design Automation Conference, pages 226-231, 2001.
H. Zhang.: SATO: An efficient propositional prover.
In Proceedings of the 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Computer Science, pages 272-275, Townsville, Australia, July 1997.
H. Zhang and J. Hsiang.: Solving open quasigroup problems by propositional reasoning.
In Proceedings of the International Computer Symp., Hsinchu, Taiwan, 1994.
L. Zhang, C. F. Madigan, M. H. Moskewicz, and S. Malik.: Efficient conflict driven learning in a boolean satisfiability solver.
In Proceedings of the International Conference on Computer Aided Design, pages 279-285, San Jose, CA, Nov. 2001. IEEE/ACM.