Accession Number : ADA326042

Title :   Algorithms for the Satisfiability (SAT) Problem: A Survey,

Corporate Author : CINCINNATI UNIV OH DEPT OF ELECTRICAL AND COMPUTER ENGINEERING

Personal Author(s) : Gu, Jun ; Purdom, Paul W. ; Franco, John ; Wah, Benjamin W.

PDF Url : ADA326042

Report Date : 1996

Pagination or Media Count : 133

Abstract : 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, database, 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.

Descriptors :   *MATHEMATICAL LOGIC, *MATHEMATICAL PROGRAMMING, ALGORITHMS, REPRINTS, ROBOTICS, OPTIMIZATION, DECISION MAKING, COMPUTER AIDED DESIGN, EXPERIMENTAL DESIGN, COMPUTER ARCHITECTURE, PARALLEL PROCESSING, SEARCHING, COMPUTER VISION, COMPUTER AIDED MANUFACTURING, COMPUTER NETWORKS.

Subject Categories : Operations Research
      Cybernetics

Distribution Statement : APPROVED FOR PUBLIC RELEASE