# SAT: references on satisfiability

# Complete methods

## Davis Putnam

Improvements to Propositional Satisfiability Search Algorithms

Freeman, J.W., PhD thesis, The University of Pennsylvania, 1995.
An Overview of Backtrack Search Satisfiability Algorithms,
João P. Marques-Silva,
in Fifth International Symposium on Artificial Intelligence and
Mathematics, January 1998.

Implementing Davis-Putnam's method by tries

Zhang, H., Stickel, M., Technical Report, The University of Iowa, 1994.

An efficient algorithm for unit-propagation

Zhang, H., Stickel, M., Proc. of the Fourth International Symposium on Artificial
Intelligence and Mathematics. Ft. Lauderdale, Florida, 1996.

SATO: An Efficient Propositional Prover

H. Zhang,
Proc. of International Conference on Automated Deduction
(CADE-97).

## Complexity analysis

A New Approach on Solving 3-Satisfiability.

R. Rodosek, Proceedings of the 3rd International
Conference on Artificial Intelligence and Symbolic Mathematical Computation,
pg 197-212, LNCS 1138, Steyr, 1996.
## Learning

Using CSP look-back
techniques to solve real world SAT instances.

R. J. Bayardo Jr. and
R. C. Schrag, Proc. of the 14th National Conf. on Artificial Intelligence, 203-208, 1997.
Using CSP look-back
techniques to solve exceptionally hard SAT instances.

R. J. Bayardo Jr. and
R. C. Schrag,
Proc. of the Second Int'l Conf. on Principles
and Practice of Constraint Programming (Lecture Notes in Computer
Science 1118) 46-60, Springer, 1996.

"Conflict Analysis in Search Algorithms for Propositional Satisfiability,"
João P. Marques-Silva and Karem A. Sakallah,
in Proceedings of the IEEE International Conference on Tools with
Artificial Intelligence, November 1996.

## Parallel solvers

Cumulating Search in a Distributed Computing Environment:
A Case Study in Parallel Satisfiability
.

Hantao Zhang and Maria Paola Bonacina. Proceedings
of First Int. Symp. on Parallel Symbolic
Computation, 1994.
PSATO: A Distributed Propositional Prover and Its
Application to Quasigroup Problems
.

Hantao Zhang, Maria Paola Bonacina and Jieh Hsiang.
Journal of Symbolic Computation, 11, 1-18, 1996.