Next: About this document ...
Up: The SAT2002 Competition (preliminary
Previous: Conclusions
- ABE00
-
Parosh Aziz Abdulla, Per Bjesse, and Niklas Eén.
Symbolic Reachability Analysis Based on SAT-Solvers.
In Proceedings of the 6th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS'2000), 2000.
- Bac02a
-
Fahiem Bacchus.
Enhancing davis putnam with extended binary clause reasoning.
In Proceedings of National Conference on Artificial Intelligence
(AAAI-2002), 2002.
to appear.
- Bac02b
-
Fahiem Bacchus.
Exploring the computational tradeoff of more reasoning and less
searching.
In SAT2002 [SAT02], pages 7-16.
- BB93
-
M. Buro and H. Kleine Büning.
Report on a SAT competition.
Bulletin of the European Association for Theoretical Computer
Science, 49:143-151, 1993.
- BCC$^+$99
-
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, M. Fujita, and Y. Zhu.
Symbolic model checking using SAT procedures instead of bdds.
In Proceedings of Design Automation Conference (DAC'99), 1999.
- BMS00
-
Luís Baptista and João P. Marques-Silva.
Using randomization and learning to solve hard real-world instances
of satisfiability.
In in Proceedings of the 6th International Conference on
Principles and Practice of Constraint Programming (CP), September 2000.
- BS97
-
Roberto J. Jr. Bayardo and Robert C. Schrag.
Using CSP look-back techniques to solve real-world SAT instances.
In Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97), pages 203-208, Providence, Rhode Island,
1997.
- CFG$^+$01
-
F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi.
Benefits of bounded model checking at an industrial setting.
In Proc. of CAV, LNCS. Springer Verlag, 2001.
- CM02
-
A. Kahng Caldwell, A. and I. Markov.
Toward cad-ip reuse: The marco gsrc bookshelf of fundamental cad
algorithms.
IEEE Design and Test, March 2002.
- CMLP02
-
B. Jurkowiak C.-M. Li and P. W. Purdom.
Integrating symmetry breaking into a dll procedure.
In SAT2002 [SAT02], pages 149-155.
- Coo71
-
Stephen A. Cook.
The complexity of theorem-proving procedures.
In Proceedings of the Third IEEE Symposium on the Foundations of
Computer Science, pages 151-158, 1971.
- CS00
-
P. Chatalic and L. Simon.
Multi-Resolution on compressed sets of clauses.
In Twelth International Conference on Tools with Artificial
Intelligence (ICTAI'00), pages 2-10, 2000.
- DABC96
-
Olivier Dubois, Pascal André, Yacine Boufkhad, and Jacques Carlier.
SAT versus UNSAT.
In Johnson and Trick [JT96], pages 415-436.
- DD01
-
Olivier Dubois and Gilles Dequen.
A backbone-search heuristic for efficient solving of hard 3-sat
formulae.
In Proceedings of the Seventeenth International Joint Conference
on Artificial Intelligence (IJCAI'01), Seattle, Washington, USA, August
4th-10th 2001.
- DGH$^+$02
-
Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon Kleinberg,
Christos Papadimitriou, Prabhakar Raghavan, and Uwe Schöning.
Deterministic
algorithm for -SAT based on
local search.
TCS, 2002.
To appear.
- DLL62
-
Martin Davis, George Logemann, and Donald Loveland.
A machine program for theorem proving.
Communications of the ACM, 5(7):394-397, July 1962.
- DP60
-
Martin Davis and Hilary Putnam.
A computing procedure for quantification theory.
Journal of the ACM, 7(3):201-215, July 1960.
- EMW97
-
Michael D. Ernst, Todd D. Millstein, and Daniel S. Weld.
Automatic SAT-compilation of planning problems.
In IJCAI97 [IJC97], pages 1169-1176.
- FAS02
-
I. Markov F. Aloul, A. Ramani and K. Sakallah.
Solving difficult sat instances in the presence of symmetry.
In Design Automation Conference (DAC), pages 731-736, New
Orleans, Louisiana, 2002.
- Fre95
-
Jon W. Freeman.
Improvements to Propositional Satisfiability Search Algorithms.
PhD thesis, Departement of computer and Information science,
University of Pennsylvania, Philadelphia, 1995.
- GN02
-
E. Goldberg and Y. Novikov.
BerkMin: A fast and robust SAT-solver.
In Design, Automation, and Test in Europe (DATE '02), pages
142-149, March 2002.
- GSK98
-
Carla P. Gomes, Bart Selman, and Henry Kautz.
Boosting combinatorial search through randomization.
In Proceedings of the Fifteenth National Conference on
Artificial Intelligence (AAAI'98), pages 431-437, Madison, Wisconsin, 1998.
- Hir00a
-
Edward A. Hirsch.
New worst-case upper bounds for SAT.
Journal of Automated Reasoning, 24(4):397-420, 2000.
Also reprinted in ``Highlights of Satisfiability Research in the Year
2000'', Volume 63 in Frontiers in Artificial Intelligence and Applications,
IOS Press, 2000.
- Hir00b
-
Edward A. Hirsch.
SAT local search algorithms: Worst-case study.
Journal of Automated Reasoning, 24(1/2):127-143, 2000.
Also reprinted in ``Highlights of Satisfiability Research in the Year
2000'', Volume 63 in Frontiers in Artificial Intelligence and Applications,
IOS Press.
- HK01
-
E. A. Hirsch and A. Kojevnikov.
UnitWalk: A new SAT solver that uses local search guided by unit
clause elimination.
PDMI preprint 9/2001, Steklov Institute of Mathematics at
St.Petersburg, 2001.
A journal version is submitted to this issue.
- Hoo94
-
J. N. Hooker.
Needed: An empirical science of algorithms.
Operations Research, 42(2):201-212, 1994.
- Hoo96
-
J. N. Hooker.
Testing heuristics: We have it all wrong.
Journal of Heuristics, pages 32-42, 1996.
- IJC97
-
Proceedings of the Fifteenth International Joint Conference on Artificial
Intelligence (IJCAI'97), Nagoya, Japan, August 23-29 1997.
- JT96
-
D. S. Johnson and M. A. Trick, editors.
Second DIMACS implementation challenge : cliques, coloring and
satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and
Theoretical Computer Science.
American Mathematical Society, 1996.
- KP92
-
Elias Koutsoupias and Christos H. Papadimitriou.
On the greedy algorithm for satisfiability.
IPL, 43(1):53-55, 1992.
- KS92
-
Henry A. Kautz and Bart Selman.
Planning as satisfiability.
In Proceedings of the Tenth European Conference on Artificial
Intelligence (ECAI'92), pages 359-363, 1992.
- KS96
-
Henry A. Kautz and Bart Selman.
Pushing the envelope : Planning, propositional logic, and stochastic
search.
In Proceedings of the Twelfth National Conference on Artificial
Intelligence (AAAI'96), pages 1194-1201, 1996.
- KS01
-
Henry Kautz and Bart Selman, editors.
Proceedings of the Workshop on Theory and Applications of
Satisfiability Testing (SAT2001), volume 9. Elsevier Science Publishers,
June 2001.
LICS 2001 Workshop on Theory and Applications of Satisfiability
Testing (SAT 2001).
- Kul02a
-
Oliver Kullmann.
First report on an adaptive density based branching rule for
DLL-like SAT solvers, using a database for mixed random conjunctive
normal forms created using the advanced encryption standard (AES).
Technical Report CSR 19-2002, University of Wales Swansea, Computer
Science Report Series, March 2002.
Extended version of [Kul02c].
- Kul02b
-
Oliver Kullmann.
Investigating the behaviour of a sat solver on random formulas.
Submitted to Annals of Mathematics and Artificial Intelligence;,
September 2002.
- Kul02c
-
Oliver Kullmann.
Towards an adaptive density based branching rule for SAT solvers,
using a database for mixed random conjunctive normal forms built upon the
advanced encryption standard (AES).
In SAT2002 [SAT02].
- LA97
-
Chu-Min Li and Anbulagan.
Heuristics based on unit propagation for satisfiability problems.
In IJCAI97 [IJC97], pages 366-371.
- LaPMS02
-
Inês Lynce and Jo ao P. Marques Silva.
Efficient data structures for backtrack search sat solvers.
In SAT2002 [SAT02].
- LBaPMS01
-
Inês Lynce, Luis Baptista, and Jo ao P. Marques Silva.
Stochastic systematic search algorithms for satisfiability.
In Kautz and Selman [KS01].
LICS 2001 Workshop on Theory and Applications of Satisfiability
Testing (SAT 2001).
- Li99
-
Chu-Min Li.
A constrained based approach to narrow search trees for
satisfiability.
Information processing letters, 71:75-80, 1999.
- Li00
-
Chu-Min Li.
Integrating Equivalency reasoning into Davis-Putnam procedure.
In Proceedings of the Seventeenth National Conference in
Artificial Intelligence (AAAI'00), pages 291-296, Austin, Texas, USA, July
30-August 3 2000.
- MMZ$^+$01
-
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
(DAC'01), pages 530-535, June 2001.
- MSS96
-
Joao P. Marques-Silva and Karem A. Sakallah.
GRASP - A New Search Algorithm for Satisfiability.
In Proceedings of IEEE/ACM International Conference on
Computer-Aided Design, pages 220-227, November 1996.
- OGMS02
-
R. Ostrowski, E. Grégoire, B. Mazure, and L. Sais.
Recovering and exploiting structural knowledge from cnf formulas.
In Proc. of the Eighth International Conference on Principles
and Practice of Constraint Programming (CP'2002), LNCS, Ithaca (N.Y.),
September 2002. Springer.
to appear.
- OVG00
-
Fumiaki Okushi and Allen Van Gelder.
Persistent and quasi-persistent lemmas in propositional model
elimination.
In (Electronic) Proc. 6th Int'l Symposium on Artificial
Intelligence and Mathematics, 2000.
To appear in special issue of Annals of Math and AI.
- PPZ97
-
R. Paturi, P. Pudlák, and F. Zane.
Satisfiability coding lemma.
In Proceedings of the 38th Annual IEEE Symposium on Foundations
of Computer Science, FOCS'97, pages 566-574, 1997.
- Pre02a
-
S. Prestwich.
A sat approach to query optimization in mediator systems.
In SAT2002 [SAT02], pages 252-259.
- Pre02b
-
S. D. Prestwich.
Randomised backtracking for linear pseudo-boolean constraint
problems.
In Proceedings of Fourth International Workshop on Integration
of AI and OR techniques in Constraint Programming for Combinatorial
Optimisation Problems, 2002.
- SAT02
-
Fifth International Symposium on the Theory and Applications of
Satisfiability Testing, Cincinnati, Ohio, USA, May 6-9, 2002 2002.
- SC01
-
Laurent Simon and Philippe Chatalic.
SATEx: a web-based framework for SAT experimentation.
In Kautz and Selman [KS01].
http://www.lri.fr/~simon/satex.
- SKC94a
-
B. Selman, H. A. Kautz, and B. Cohen.
Noise strategies for improving local search.
In Proceedings of the 12th National Conference on Artificial
Intelligence, AAAI'94, pages 337-343, 1994.
- SKC94b
-
Bart Selman, Henry A. Kautz, and Bram Cohen.
Noise strategies for improving local search.
In Proceedings of the Twelfth National Conference on Artificial
Intelligence (AAAI'94), pages 337-343, Seattle, 1994.
- SLM92
-
B. Selman, H. Levesque, and D. Mitchell.
A new method for solving hard satisfiability problems.
In Proceedings of the 10th National Conference on Artificial
Intelligence, AAAI'92, pages 440-446, 1992.
- SS01
-
Geoff Sutcliff and Christian Suttner.
Evaluating general purpose automated theorem proving systems.
Artificial Intelligence, 131:39-54, 2001.
- SSWH02
-
Rainer Schuler, Uwe Schöning, Osamu Watanabe, and Thomas Hofmeister.
A probabilistic 3-SAT algorithm further improved.
In Proceedings of 19th International Symposium on Theoretical
Aspects of Computer Science, STACS 2002, Lecture Notes in Computer Science.
Springer, 2002.
- SW98
-
Y. Shang and B. W. Wah.
A discrete lagrangian-based global-search method for solving
satisfiability problems.
Journal of Global Optimization, 12(1):61-99, January 1998.
- Tse68
-
G. S. Tseitin.
On the complexity of derivation in the propositional calculus.
Zapiski nauchnykh seminarov LOMI, 8:234-259, 1968.
English translation of this volume: Consultants Bureau, N.Y., 1970,
pp. 115-125.
- Urq87
-
Alasdair Urquhart.
Hard examples for resolution.
Journal of the Association for Computing Machinery,
34(1):209-219, 1987.
- VB01
-
M.N. Velev and R.E. Bryant.
Effective use of boolean satisfiability procedures in the formal
verification of superscalar and vliw microprocessors.
In Proceedings of the 38th Design Automation Conference (DAC
'01), pages 226-231, June 2001.
- VG99
-
A. Van Gelder.
Autarky pruning in propositional model elimination reduces failure
redundancy.
Journal of Automated Reasoning, 23(2):137-193, 1999.
- VG02a
-
Allen Van Gelder.
Extracting (easily) checkable proofs from a satisfiability solver
that employs both preorder and postorder resolution.
In Seventh Int'l Symposium on AI and Mathematics, Ft. Lauderdale, FL, 2002.
- VG02b
-
Allen Van Gelder.
Generalizations of watched literals for backtracking search.
In Seventh Int'l Symposium on AI and Mathematics, Ft. Lauderdale, FL, 2002.
- VGO99
-
A. Van Gelder and F. Okushi.
Lemma and cut strategies for propositional model elimination.
Annals of Mathematics and Artificial Intelligence,
26(1-4):113-132, 1999.
- VT96
-
Allen Van Gelder and Yumi K. Tsuji.
Satisfiability Testing with More Reasoning and Less Guessing.
In Johnson and Trick [JT96], pages 559-586.
- WvM00
-
Joost Warners and Hans van Maaren.
Solving satisfiability problems using elliptic approximations:
effective branching rules.
Discrete Applied Mathematics, 107:241-259, 2000.
- Zha97
-
Hantao Zhang.
SATO: an efficient propositional prover.
In Proceedings of the International Conference on Automated
Deduction (CADE'97), volume 1249 of LNAI, pages 272-275, 1997.
- ZMMM01
-
L. Zhang, C. F. Madigan, M. W. Moskewicz, and S. Malik.
Efficient conflict driven learning in a Boolean satisfiability
solver.
In International Conference on Computer-Aided Design
(ICCAD'01), pages 279-285, November 2001.
- ZS96
-
H. Zhang and M. E. Stickel.
An efficient algorithm for unit propagation.
In Proceedings of the Fourth International Symposium on
Artificial Intelligence and Mathematics (AI-MATH'96), Fort Lauderdale
(Florida USA), 1996.
- ZS02
-
L. Zheng and P. J. Stuckey.
Improving SAT using 2SAT.
In Michael J. Oudshoorn, editor, Proceedings of the Twenty-Fifth
Australasian Computer Science Conference (ACSC2002), Melbourne, Australia,
2002. ACS.
LE BERRE Daniel
2002-09-16