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].

For the entire collection see [Zbl 0881.00041].

##### MSC:

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 |