SAT: references on satisfiability

collected by

ipg@cs.strath.ac.uk

tw@cs.strath.ac.uk

Beyond the propositional

OBDDs

Ordere d binary decision diagrams and the Davis-Putnam procedure.
Uribe, T.E. and M.E. Stickel, Proceedings of the First International Conference on Constraints in Computational Logics, Munich, Germany, September 1994, 34-49.

Linear 0-1

Solving Linear Pseudo-Boolean Constraint Problems with Local Search.
J. Walser, Proceedings of the 14th National Conference on Artificial Intelligence, AAAI-97 Providence, RI, 1997.

A Davis-Putnam Based Enumeration Algorithm for Linear pseudo-Boolean Optimization.
P. Barth, MPI Technical Report, MPI-I-95-2-003, 1995.

Pseudo-Boolean and Finite Domain Constraint Programming: A Case Study.
A. Bockmayr and T. Kasper, MPI Technical Report, 1996.

Modelling 0-1 problems in CLP(PB).
P. Barth and A. Bockmayr, MPI Technical Report, 1996.

Modal logic

Building decision procedures for modal logics from propositional decision procedures - the case study of modal K.
F. Giunchiglia and R. Sebastiani, Proceedings of 13th International Conference on Automated Deduction (CADE-13), Lecture Notes on Artificial Intelligence series. New Brunswick, New Jersey, USA, 1996.

A SAT-based decision procedure for ALC.
F. Giunchiglia and R. Sebastiani, Proceedings "5th International Conference on Principl es of Knowledge Representation and Reasoning - KR'96, 1996.

A new method for testing decision procedures in modal and terminological logics.
F. Giunchiglia, M. Roveri and R. Sebastiani, 1996 International Workshop on Description Logics - DL'96. Boston, MA, USA, 1996. Short version also published in Proceedings 14th International Conference on Automated Deduction (CADE-14) with the title "A new method for testing decision procedures in modal logics".

QSAT

Beyond NP: the QSAT phase transition
Ian Gent and Toby Walsh. Technical report, APES-05-1998, July 1998. To appear in Proceedings of AAAI-99.

An Algorithm to Evaluate Quantified Boolean Formulae.
M. Cadoli, A. Giovanardi, M. Schaerf, Proceedings of AAAI-98, July, 1998.

Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae.
M. Cadoli, A. Giovanardi, M. Schaerf. Proc. of AI*IA-97, Springer LNAI, 1997.

An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation.
M. Cadoli, M. Schaerf, A. Giovanardi, M. Giovanardi. Technical report DIS 08-99, March 1999. Significantly extended version of AI*IA-97 and AAAI-98.

Improvements to the evaluation of quantified Boolean formulae
J. Rintanen, Proceedings of the 16th International Joint Conference in Artificial Intelligence, Stockholm, Sweden, August 1999.

First order logic

ModGen: Theorem proving by model generation
S. Kim and H. Zhang, Proc. of National Conference of American Association on Artificial Intelligence (AAAI-94), Seattle, WA. MIT Press, pp. 162-167.