ccisdefined journalfont
-
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í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.
Journal of Artificial Intelligence Research 22 (2004). Copyright AI Access Foundation. All rights reserved.