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 SATSolvers.
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
(AAAI2002), 2002.
to appear.
 Bac02b

Fahiem Bacchus.
Exploring the computational tradeoff of more reasoning and less
searching.
In SAT2002 [SAT02], pages 716.
 BB93

M. Buro and H. Kleine Büning.
Report on a SAT competition.
Bulletin of the European Association for Theoretical Computer
Science, 49:143151, 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. MarquesSilva.
Using randomization and learning to solve hard realworld 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 lookback techniques to solve realworld SAT instances.
In Proceedings of the Fourteenth National Conference on
Artificial Intelligence (AAAI'97), pages 203208, 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 cadip 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 149155.
 Coo71

Stephen A. Cook.
The complexity of theoremproving procedures.
In Proceedings of the Third IEEE Symposium on the Foundations of
Computer Science, pages 151158, 1971.
 CS00

P. Chatalic and L. Simon.
MultiResolution on compressed sets of clauses.
In Twelth International Conference on Tools with Artificial
Intelligence (ICTAI'00), pages 210, 2000.
 DABC96

Olivier Dubois, Pascal André, Yacine Boufkhad, and Jacques Carlier.
SAT versus UNSAT.
In Johnson and Trick [JT96], pages 415436.
 DD01

Olivier Dubois and Gilles Dequen.
A backbonesearch heuristic for efficient solving of hard 3sat
formulae.
In Proceedings of the Seventeenth International Joint Conference
on Artificial Intelligence (IJCAI'01), Seattle, Washington, USA, August
4th10th 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):394397, July 1962.
 DP60

Martin Davis and Hilary Putnam.
A computing procedure for quantification theory.
Journal of the ACM, 7(3):201215, July 1960.
 EMW97

Michael D. Ernst, Todd D. Millstein, and Daniel S. Weld.
Automatic SATcompilation of planning problems.
In IJCAI97 [IJC97], pages 11691176.
 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 731736, 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 SATsolver.
In Design, Automation, and Test in Europe (DATE '02), pages
142149, 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 431437, Madison, Wisconsin, 1998.
 Hir00a

Edward A. Hirsch.
New worstcase upper bounds for SAT.
Journal of Automated Reasoning, 24(4):397420, 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: Worstcase study.
Journal of Automated Reasoning, 24(1/2):127143, 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):201212, 1994.
 Hoo96

J. N. Hooker.
Testing heuristics: We have it all wrong.
Journal of Heuristics, pages 3242, 1996.
 IJC97

Proceedings of the Fifteenth International Joint Conference on Artificial
Intelligence (IJCAI'97), Nagoya, Japan, August 2329 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):5355, 1992.
 KS92

Henry A. Kautz and Bart Selman.
Planning as satisfiability.
In Proceedings of the Tenth European Conference on Artificial
Intelligence (ECAI'92), pages 359363, 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 11941201, 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
DLLlike SAT solvers, using a database for mixed random conjunctive
normal forms created using the advanced encryption standard (AES).
Technical Report CSR 192002, 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

ChuMin Li and Anbulagan.
Heuristics based on unit propagation for satisfiability problems.
In IJCAI97 [IJC97], pages 366371.
 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

ChuMin Li.
A constrained based approach to narrow search trees for
satisfiability.
Information processing letters, 71:7580, 1999.
 Li00

ChuMin Li.
Integrating Equivalency reasoning into DavisPutnam procedure.
In Proceedings of the Seventeenth National Conference in
Artificial Intelligence (AAAI'00), pages 291296, Austin, Texas, USA, July
30August 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 530535, June 2001.
 MSS96

Joao P. MarquesSilva and Karem A. Sakallah.
GRASP  A New Search Algorithm for Satisfiability.
In Proceedings of IEEE/ACM International Conference on
ComputerAided Design, pages 220227, 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 quasipersistent 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 566574, 1997.
 Pre02a

S. Prestwich.
A sat approach to query optimization in mediator systems.
In SAT2002 [SAT02], pages 252259.
 Pre02b

S. D. Prestwich.
Randomised backtracking for linear pseudoboolean 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 69, 2002 2002.
 SC01

Laurent Simon and Philippe Chatalic.
SATEx: a webbased 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 337343, 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 337343, 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 440446, 1992.
 SS01

Geoff Sutcliff and Christian Suttner.
Evaluating general purpose automated theorem proving systems.
Artificial Intelligence, 131:3954, 2001.
 SSWH02

Rainer Schuler, Uwe Schöning, Osamu Watanabe, and Thomas Hofmeister.
A probabilistic 3SAT 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 lagrangianbased globalsearch method for solving
satisfiability problems.
Journal of Global Optimization, 12(1):6199, January 1998.
 Tse68

G. S. Tseitin.
On the complexity of derivation in the propositional calculus.
Zapiski nauchnykh seminarov LOMI, 8:234259, 1968.
English translation of this volume: Consultants Bureau, N.Y., 1970,
pp. 115125.
 Urq87

Alasdair Urquhart.
Hard examples for resolution.
Journal of the Association for Computing Machinery,
34(1):209219, 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 226231, June 2001.
 VG99

A. Van Gelder.
Autarky pruning in propositional model elimination reduces failure
redundancy.
Journal of Automated Reasoning, 23(2):137193, 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(14):113132, 1999.
 VT96

Allen Van Gelder and Yumi K. Tsuji.
Satisfiability Testing with More Reasoning and Less Guessing.
In Johnson and Trick [JT96], pages 559586.
 WvM00

Joost Warners and Hans van Maaren.
Solving satisfiability problems using elliptic approximations:
effective branching rules.
Discrete Applied Mathematics, 107:241259, 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 272275, 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 ComputerAided Design
(ICCAD'01), pages 279285, 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 (AIMATH'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 TwentyFifth
Australasian Computer Science Conference (ACSC2002), Melbourne, Australia,
2002. ACS.
LE BERRE Daniel
20020916