next up previous
Next: About this document ... Up: The SAT2002 Competition (preliminary Previous: Conclusions

Bibliography

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 $ (2-2/(k+1))^n$ algorithm for $ k$-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