Here is some of SAT papers we
collected (mostly from SATLIB):
 Bayardo Jr., R. J.; Schrag, R. C. Using
CSP lookback techniques to solve real world SAT instances. In: Proc. of
the 14th National Conf. on Artificial Intelligence, pp. 203208, 1997.
[ SAT, complete algorithms, learning. ]
 Barth, P. A DavisPutnam Based
Enumeration Algorithm for Linear pseudoBoolean Optimization.
MPI Technical Report, MPII952003, 1995.
[ SAT, complete algorithms, Davis Putnam, constraint programming, 01
problems. ]
 Barth, P.; Bockmayr, A. Modelling 01
problems in CLP(PB). MPI Technical Report, 1996.
[ Constraint programming, 01 problems. ]
 Bockmayr, A.; Kasper, T. PseudoBoolean
and Finite Domain Constraint Programming: A Case Study. MPI Technical
Report, 1996.
[ Constraint programming, 01 problems. ]
 Bayardo Jr., R. J.; Schrag, R. C. Using
CSP lookback techniques to solve exceptionally hard SAT instances. In:
Proc. of the Second Int'l Conf. on Principles and Practice of Constraint
Programming (Lecture Notes in Computer Science 1118), pp. 4660, Springer,
1996.
[ SAT, complete algorithms, learning. ]
 Beringer, A.; Aschemann, G.; Hoos, Holger H.; Metzger, M.; Weiß, A. GSAT
versus Simulated Annealing. In: Proc. of ECAI'94, pp. 130134, John
Wiley \& Sons, 1994.
[SAT, local search, random 3sat, simulated annealing. ]
 Cadoli, M.; Giovanardi, A.; Schaerf, M. Experimental
Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae.
Proc. of AI*IA97, Springer LNAI, 1997.
[ QSAT, algorithms, empirical analysis. ]
 Cadoli, M.; Giovanardi, A.; Schaerf, M. An
Algorithm to Evaluate Quantified Boolean Formulae. Proceedings of
AAAI98, July, 1998.
[ QSAT, algorithms. ]
 Cadoli, M.; Schaerf, M.; Giovanardi, A.; Giovanardi, M. An
Algorithm to Evaluate Quantified Boolean Formulae and its Experimental
Evaluation. Technical report DIS 0899, March 1999. Significantly
extended version of AI*IA97 and AAAI98.
[ QSAT, algorithms, empirical analysis. ]
 Clark, Dave; Frank, Jeremy; Gent, Ian; MacIntyre, Ewan; Tomov, Neven;
Walsh, Toby. Local
Search and the Number of Solutions. Proceedings of CP96, 1996.
[ SAT, local search, search behaviour, search space analysis,
empirical analysis. ]
 Cook, S.A.; Mitchell, D.G.
Finding Hard Instances of the Satisfiability Problem: A Survey
. In: "Satisfiability Problem: Theory and Applications", DIMACS
Series in Discrete Mathematics and Theoretical Computer Science, American
Mathematical Society, 1997.
[ SAT, survey article, applications, hard instances. ]
 Frank, J. Weighting
for Godot: Learning heuristics for GSAT. J. Frank, Proc. AAAI96.
[ SAT, local search algorithms, GSAT, clause weighting. ]
 Freeman, J.W. Improvements
to Propositional Satisfiability Search Algorithms . PhD thesis, The
University of Pennsylvania, 1995.
[ SAT, complete algorithms, Davis Putnam. ]
 Gent, I.; Walsh, T. An
Empirical Analysis of Search in GSAT. Journal
of Artificial Intelligence Research, Vol.
1, September 1993.
[ SAT, local search algorithms, GSAT. ]
 Gent, Ian; MacIntyre, Ewan; Prosser, Patrick; Walsh, Toby. The
Constrainedness of Search. Proceedings of AAAI96, pages 246252, 1996.
[ SAT, search, constrainedness, phase transition. ]
 Gent, I.; Walsh, T. Towards
an Understanding of Hillclimbing Procedures for SAT. Proceedings of
AAAI93.
[ SAT, local search algorithms, GenSAT. ]
 Gent, I.; Walsh, T. Unsatisfied
Variables in Local Search. In `Hybrid Problems, Hybrid Solutions'
(Proceedings of AISB95), Ed. J. Hallam, IOS Press, Amsterdam, 1995, pages
7385.
[ SAT, local search algorithms, random walk. ]
 Gent, Ian; Walsh, Toby. The
SAT Phase Transition. Proceedings of ECAI94, ed. A G Cohn, John Wiley
& Sons, 105109, 1994.
[ SAT, phase transition, random 3sat. ]
 Gent, Ian; Walsh, Toby. Easy
Problems are Sometimes Hard. Artificial Intelligence, 70, 335345, 1994.
[ SAT, phase transition, constant probability model. ]
 Gent, Ian; Walsh, Toby. The
Satisfiability Constraint Gap. Artificial Intelligence, 81 (12), 1996.
[ SAT, phase transition, random 3sat. ]
 Gent, Ian; Walsh, Toby. Beyond
NP: the QSAT phase transition. Technical report, APES051998, July
1998. To appear in Proceedings of AAAI99.
[ QSAT, phase transition, empirical analysis. ]
 Gent, Ian; Walsh, Toby.
The Search for Satisfaction. Draft paper, 1999.
[ SAT, survey article. ]
 Giunchiglia, F.; Sebastiani, R. Building
decision procedures for modal logics from propositional decision procedures
 the case study of modal K. Proceedings of 13th International
Conference on Automated Deduction (CADE13), Lecture Notes on Artificial
Intelligence series. New Brunswick, New Jersey, USA, 1996.
[ SAT, modal logic, complete algorithms. ]
 Giunchiglia, F.; Sebastiani, R. A
SATbased decision procedure for ALC. Proceedings of the 5th
International Conference on Principles of Knowledge Representation and
Reasoning  KR'96, 1996.
[ SAT, modal logic, complete algorithms. ]
 Giunchiglia, F; Roveri, M.; Sebastiani, R. A
new method for testing decision procedures in modal and terminological
logics. 1996 International Workshop on Description Logics  DL'96.
Boston, MA, USA, 1996. Short version also published in Proceedings 14th
International Conference on Automated Deduction (CADE14) with the title
"A new method for testing decision procedures in modal logics".
[ SAT, modal logic, complete algorithms. ]
 Guerra e Silva, Lu¨Ēs; MarquesSilva, João P.; Silveira, Lu¨Ēs M.;
Sakallah, Karem A. Timing
Analysis Using Propositional Satisfiability. Proceedings of the IEEE
International Conference on Electronics, Circuits and Systems (ICECS),
September 1998.
[ SAT, applications, hardware. ]
 Gu, J.; Purdom, P.W.; Franco, J.; Wah, B.W.
Algorithms for the Satisfiability (SAT) Problem: A Survey
. In: "Satisfiability Problem: Theory and Applications", DIMACS
Series in Discrete Mathematics and Theoretical Computer Science, American
Mathematical Society, pp. 19152, 1997.
[ SAT, survey article, algorithms. ]
 Guerra e Silva, Lu¨Ēs; MarquesSilva, João P.; Silveira, Lu¨Ēs M.;
Sakallah, Karem A. Realistic
Delay Modeling in SatisfiabilityBased Timing Analysis, Proceedings of
the IEEE International Symposium on Circuits and Systems (ISCAS), May 1998.
[ SAT, applications, hardware. ]
 Hogg, T.; Huberman, B. A.; Williams, C. Phase
Transitions and the Search Problem. Tutorial paper, 1996.
[ SAT, search, phase transition. ]
 Hoos, Holger H. SATEncodings,
Search Space Structure, and Local Search Performance. In: Proc. of
IJCAI'99, pp. 296302, Morgan Kaufmann, 1999.
[SAT, local search, encodings, empirical analysis, search space
analysis. ]
 Hoos, Holger H. On
the Runtime Behaviour of Stochastic Local Search Algorithms for SAT.
In: Proc. of AAAI, pp. 661666, MIT Press, 1999.
[SAT, local search, encodings, search behaviour, empirical analysis.
]
 Hoos, Holger H. Stochastic
Local Search  Methods, Models, Applications. PhD thesis, TU Darmstadt,
1998.
[ SAT, local search, random 3sat, search behaviour, empirical
analysis, parallel algorithms, applications, planning, search space
analysis. ]
 Hoos, Holger H.; St¨štzle, Thomas. Towards
a Characterisation of the Behaviour of Stochastic Local Search Algorithms
for SAT.. Artificial Intelligence, 112, 213232, 1999.
[ SAT, phase transition, constant probability model. ]
 Hoos, Holger H.; St¨štzle, Thomas Local
Search Algorithms for SAT: An Empirical Evaluation.. To appear in
Journal of Automated Reasoning, 2000.
[SAT, local search, search behaviour, empirical analysis.]
 Hoos, Holger H.; St¨štzle, Thomas SATLIB:
An Online Resource for Research on SAT.. In: SAT 2000, Ian Gent, Hans
van Maaren, and Toby Walsh, editors, IOS Press. 2000.
[SAT, benchmark libraries, research resources.]
 Hoos, Holger H. Solving
Hard Combinatorial Problems with GSAT  A Case Study.. In: Proceedings
of the German Conference on Artificial Intelligence (KI'96), pp. 197212,
LNCS 1138, 1996.
[SAT, local search, graph colouring.]
 Jiang, Yueyun; Kautz, Henry; Selman, Bart. Solving
Problems with Hard and Soft Constraints Using A Stochastic Algorithm for
MAXSAT". 1st International Joint Workshop on Artificial
Intelligence and Operations Research, 1995.
[ MAXSAT, applications, steiner trees. ]
 Kautz, Henry; McAllester, David; Selman, Bart. Encoding
Plans in Propositional Logic. Proceedings KR96, 1996.
[ SAT, applications, planning. ]
 Kautz, Henry; Selman, Bart. Planning
as Satisfiability. Proceedings ECAI92, 1992.
[ SAT, applications, planning. ]
 Kautz, Henry; Selman, Bart. Pushing
the Envelope: Planning, Propositional Logic, and Stochastic Search.
Proceedings AAAI96, 1996
[ SAT, applications, planning. ]
 Kautz, Henry; Selman, Bart. BLACKBOX:
A New Approach to the Application of Theorem Proving to Problem Solving.
Working notes of the Workshop on Planning as Combinatorial Search, held in
conjunction with AIPS98, Pittsburgh, PA, 1998.
[ SAT, applications, planning. ]
 Kautz, Henry; Selman, Bart. The
Role of DomainSpecific Knowledge in the Planning as Satisfiability
Framework. Proceedings of AIPS98, Pittsburgh, PA, 1998.
[ SAT, applications, planning. ]
 Kautz, Henry; Selman, Bart; Jiang, Yueyun. General
Stochastic Approach to Solving Problems with Hard and Soft Constraints".
In The Satisfiability Problem: Theory and Applications, Dingzhu Gu,
Jun Du, and Panos Pardalos (Eds.), DIMACS Series in Discrete Mathematics and
Theoretical Computer Science, vol. 35, American Mathematical Society, 1997,
pages 573586.
[ MAXSAT, applications, steiner trees. ]
 Kim, S.; Zhang, H. ModGen:
Theorem proving by model generation. Proc. of National Conference of
American Association on Artificial Intelligence (AAAI94), Seattle, WA. MIT
Press, pp. 162167.
[ SAT, First order logic, theorem proving, model generation. ]
 Kirousis, L. M.; Kranakis, E.; Krizanc. D. A
Better Upper Bound for the Unsatisfiability Threshold. Technical report
TR9609, School of Computer Science, Carleton University, 1996.
[ SAT, phase transition, random 3sat. ]
 van Maaren, Hans. Highlights
of Satisfiability Research in the Year 2000  Preface. In: SAT 2000 
Highlights of Satisfiability Research in the Year 2000, Ian Gent, Hans van
Maaren, and Toby Walsh, editors, IOS Press. 2000.
[ SAT, survey article. ]
 MarquesSilva, João P. Search
Algorithms for Satisfiability Problems in Combinational Switching Circuits.
Ph.D. Dissertation, EECS Department, University of Michigan, May 1995.
[ SAT, applications, hardware. ]
 MarquesSilva, João P. An
Overview of Backtrack Search Satisfiability Algorithms. In: Fifth
International Symposium on Artificial Intelligence and Mathematics, January
1998.
[ SAT, complete algorithms, Davis Putnam. ]
 MarquesSilva, João P.; Sakallah, Karem A. Conflict
Analysis in Search Algorithms for Propositional Satisfiability. In:
Proceedings of the IEEE International Conference on Tools with Artificial
Intelligence, November 1996.
[ SAT, complete algorithms, learning. ]
 MarquesSilva, João P.; Sakallah, Karem A. Robust
Search Algorithms for Test Pattern Generation. Proceedings of the IEEE
FaultTolerant Computing Symposium, June 1997.
[ SAT, applications, hardware. ]
 McAllester, D.; Selman, B.; Kautz, H. Evidence
for Invariants in Local Search. Proc. AAAI97, Providence, RI, 1997.
[ SAT, local search algorithms, WalkSAT. ]
 Mitchell, David; Selman, Bart; Levesque, Hector. Hard
and Easy Distribution of SAT Problems. Proceedings AAAI92, 1992.
[ SAT, phase transition, random 3sat. ]
 Parkes, A.J.; Walser, J. Tuning
Local Search for Satisfiability Testing. Proceedings of the 13th
National Conference on Artificial Intelligence, Portland, OR, 1996.
[ SAT, local search, WalkSAT, empirical analysis, random3sat. ]
 Rintanen, J. Improvements
to the evaluation of quantified Boolean formulae. Proceedings of the
16th International Joint Conference in Artificial Intelligence, Stockholm,
Sweden, August 1999.
[ QSAT, algorithms. ]
 Rodosek, R. A
New Approach on Solving 3Satisfiability. In: Proceedings of the 3rd
International Conference on Artificial Intelligence and Symbolic
Mathematical Computation, pp. 197212, LNCS 1138, Steyr, 1996.
[ SAT, complete algorithms, complexity analysis. ]
 Selman, B.; Kautz, H. An
Empirical Study of Greedy Local Search for Satisfiability Testing. Proc.
AAAI93.
[ SAT, local search algorithms, GSAT, clause weighting. ]
 Selman, B.; Kautz, H. DomainIndependent
Extensions to GSAT: Solving Large Structured Satisfiability Problems.
Proc. IJCAI93.
[ SAT, local search algorithms, GSAT, random walk. ]
 Selman, B.; Kautz, H.; Cohen, B. Local
Search Strategies for Satisfiability Testing. Proceedings of 2nd DIMACS
Challenge on Cliques, Coloring and Satisfiability, 1994.
[ SAT, local search algorithms, WalkSAT. ]
 Selman, B.; Levesque, H.; Mitchell, D. GSAT
 A New Method for Solving Hard Satisfiability Problems. Proceedings
AAAI92.
[ SAT, local search algorithms, GSAT. ]
 Singer, Josh; Gent, Ian; Smaill, Alan. Backbone
Fragility and the Local Search Cost Peak. Journal
of Artificial Intelligence Research, Vol. 12, pp. 235270, 2000.
[ SAT, local search, search behaviour, search space analysis,
empirical analysis, phase transition, random 3sat, WalkSAT. ]
 Slaney, J.; Fujita, M.; Stickel, M. Automated
reasoning and exhaustive search: quasigroup existence problems.
Computers and Mathematics with Applications 29, 115132, 1995.
[ SAT, applications, quasigroup existence. ]
 Steinmann, Olaf; Strohmeier, Antje; St¨štzle, Thomas. Tabu
Search vs. Random Walk. KI97: Advances in Artificial Intelligence,
Springer Verlag, LNCS, Vol. 1303, 1997
[ SAT, local search, tabu search, random walk, constraint
satisfaction. ]
 Uribe, T.E.; Stickel, M.E. Ordered
binary decision diagrams and the DavisPutnam procedure. Proceedings of
the First International Conference on Constraints in Computational Logics,
Munich, Germany, September 1994, 3449.
[ SAT, complete algorithms, Davis Putnam, OBDDs. ]
 Walser, Joachim. Solving
Linear PseudoBoolean Constraint Problems with Local Search. Proceedings
of the 14th National Conference on Artificial Intelligence, AAAI97,
Providence, RI, 1997.
[ SAT, local search, WalkSAT, constraint programming, 01 problems. ]
 Zhang, H. SATO:
An Efficient Propositional Prover. Proc. of International Conference on
Automated Deduction (CADE97), 1997.
[ SAT, complete algorithms, Davis Putnam. ]
 Zhang, Hantao. Specifying
Latin Square Problems in Propositional Logics.
[ SAT, applications, quasigroup existence. ]
 Zhang, H.; Bonacina, Maria Paola. Cumulating
Search in a Distributed Computing Environment: A Case Study in Parallel
Satisfiability.. In: Proceedings of First Int. Symp. on Parallel
Symbolic Computation, 1994.
[ SAT, complete algorithms, parallel algorithms. ]
 Zhang, Hantao; Bonacina, Maria Paola; Hsiang, Jieh. PSATO:
A Distributed Propositional Prover and Its Application to Quasigroup
Problems. Journal of Symbolic Computation, 11, 118, 1996.
[ SAT, complete algorithms, parallel algorithms. ]
 Zhang, Hantao; Hsiang, Jieh. Solving
Open Quasigroup Problems by Propositional Reasoning.
[ SAT, applications, quasigroup existence. ]
 Zhang, H.; Stickel, M. Implementing
DavisPutnam's method by tries. Technical Report, The University of
Iowa, 1994.
[ SAT, complete algorithms, Davis Putnam. ]
 Zhang, H.; Stickel, M. An
efficient algorithm for unitpropagation. In: Proc. of the Fourth
International Symposium on Artificial Intelligence and Mathematics. Ft.
Lauderdale, Florida, 1996.
[ SAT, complete algorithms, Davis Putnam. ]
