zbMATH — the first resource for mathematics

Algorithms for the satisfiability (SAT) problem: A survey. (English) Zbl 0945.03040
Du, Dingzhu (ed.) et al., Satisfiability problem: theory and applications. DIMACS workshop, Piscataway, NJ, USA, March 11-13, 1996. Providence, RI: AMS, American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 35, 19-151 (1997).
Summary: The satisfiability (SAT) problem is a core problem in mathematical logic and computing theory. In practice, SAT is fundamental in solving many problems in automated reasoning, computer-aided design, computer-aided manufacturing, machine vision, databases, robotics, integrated circuit design, computer architecture design, and computer network design. Traditional methods treat SAT as a discrete, constrained decision problem. In recent years, many optimization methods, parallel algorithms, and practical techniques have been developed for solving SAT. In this survey, we present a general framework (an algorithm space) that integrates existing SAT algorithms into a unified perspective. We describe sequential and parallel SAT algorithms including variable splitting, resolution, local search, global optimization, mathematical programming, and practical SAT algorithms. We give performance evaluation of some existing SAT algorithms. Finally, we provide a set of practical applications of the satisfiability problems.
For the entire collection see [Zbl 0881.00041].

03B70 Logic in computer science
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
90C27 Combinatorial optimization
90C90 Applications of mathematical programming
68W99 Algorithms in computer science
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
68-02 Research exposition (monographs, survey articles) pertaining to computer science
03B05 Classical propositional logic
03B25 Decidability of theories and sets of sentences
68Q25 Analysis of algorithms and problem complexity
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q42 Grammars and rewriting systems
MINOS; Walksat; Genocop