Last page LERIA Faculty of Sciences University of Angers
Version française


What is the SAT problem?


The satisfiability problem (SAT) [6] consists in finding a truth assignment that satisfies a well-formed Boolean expression. An instance of the SAT problem is defined by a set of boolean variables (also called atoms) ${\cal X} = \{x_1,...,x_n\}$ and a boolean formula $\phi \colon \{0,1\}^n \to \{0,1\}$. A literal is a variable or its negation. A (truth) assignment is a function $v \colon {\cal X} \to \{0,1\}$. The formula is said to be satisfiable if there exists an assignment satisfying $\phi$ and unsatisfiable otherwise. The formula $\phi$ is in conjunctive normal form (CNF) if it is a conjunction of clauses where a clause is a disjunction of literals. In this paper, $\phi$ is supposed to be in CNF. SAT is originally stated as a decision problem but we are also interesting here in the MAX-SAT problem which consists in finding an assignment which satisfies the maximum number of clauses in $\phi$.
SAT has many practical applications (VLSI test and verification, consistency maintenance, fault diagnosis, planning ...). During the last decade, several improved solution algorithms have been developed and important progress has been achieved. These algorithms can be divided into two main classes:

Complete algorithms: Designed to solve the initial decision problem, the most powerful complete algorithms are based on the Davis-Putnam-Loveland procedure [2]. They differ essentially by the underlying heuristic used for the branching rule [12,15]. Specific techniques such as symmetry-breaking, backbone detecting or equivalence elimination are also used to reinforce these algorithms [1,4,11].

Incomplete algorithms: They are mainly based on local search [8,10,13,14] and evolutionary algorithms [3,5,7]. Walksat [13] and UnitWalk [9] are famous examples of incomplete algorithms. Though incomplete algorithms are little helpful for unsatisfiable instances, they represent the unique approach for finding models of very large instances.


Bibliography

1
Belaid Benhamou and Lakhdar Sais.
Theoretical study of symmetries in propositional calculus and applications.
In CADE'92, pages 281-294, 1992.

2
Martin Davis, George Logemann, and Donald Loveland.
A machine program for theorem-proving.
Communications of the ACM, 5(7):394-397, Jul 1962.

3
Kenneth A. De Jong and William M. Spears.
Using genetic algorithm to solve NP-complete problems.
In Proc. of the Third Int. Conf. on Genetic Algorithms, pages 124-132, San Mateo, CA, 1989.

4
Olivier Dubois and Gilles Dequen.
A backbone-search heuristic for efficient solving of hard 3-SAT formulae.
In Bernhard Nebel, editor, Proc. of the IJCAI'01, pages 248-253, San Francisco, CA, 2001.

5
Charles Fleurent and Jacques A. Ferland.
Object-oriented implementation of heuristic search methods for graph coloring, maximum clique, and satisfiability.
In Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 619-652, 1994.

6
Michael R. Garey and David S. Johnson.
Computers and Intractability , A Guide to the Theory of NP-Completeness.
W.H. Freeman & Company, San Francisco, 1978.

7
Jens Gottlieb, Elena Marchiori, and Claudio Rossi.
Evolutionary algorithms for the satisfiability problem.
Evolutionary Computation, 10(1):35-50, 2002.

8
Pierre Hansen and Brigitte Jaumard.
Algorithms for the maximum satisfiability problem.
Computing, 44(4):279-303, 1990.

9
Edward A. Hirsch and Arist 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.

10
Brigitte Jaumard, Mihnea Stan, and Jacques Desrosiers.
Tabu search and a quadratic relaxation for the satisfiability problem.
In Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 457-478, 1994.

11
Chu Min Li.
Integrating equivalency reasoning into davis-putnam procedure.
In Proc. of the AAAI'00, pages 291-296, 2000.

12
Chu Min Li and Anbulagan.
Heuristics based on unit propagation for satisfiability problems.
In Proc. of the IJCAI'97, pages 366-371, 1997.

13
Bart Selman, Henry A. Kautz, and Bram Cohen.
Noise strategies for improving local search.
In Proc. of the AAAI, Vol. 1, pages 337-343, 1994.

14
William M. Spears.
Simulated annealing for hard satisfiability problems.
In Second DIMACS implementation challenge : cliques, coloring and satisfiability, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 533-558, 1996.

15
Hantao Zhang.
SATO: An efficient propositional prover.
In Proc. of the 14th International Conference on Automated deduction, volume 1249 of LNAI, pages 272-275, Berlin, 1997.