8 - Boolean satisfiability and EDA applications

Summary

Introduction

Boolean satisfiability (SAT) is a widely used modeling framework for solving combinatorial problems. It is also a well-known decision problem in theoretical computer science, being the first problem to be shown to be NP-complete. [11] Since SAT is NP-complete, and unless P=NP, all SAT algorithms require worst-case exponential time. However, modern SAT algorithms are extremely effective at coping with large search spaces, by exploiting the problem's structure when it exists. [2–4] The performance improvements made to SAT solvers since the mid 1990s motivated their application to a wide range of practical applications, from cross-talk noise prediction in integrated circuits [5] to termination analysis in term-rewrite systems. [6] In some applications, the use of SAT provides remarkable performance improvements. Examples include model-checking of finite-state systems, [7–9] design debugging, [10] AI planning, [11,12] and haplotype inference in bioinformatics. [13] Additional successful examples of practical applications of SAT include termination analysis in term-rewrite systems, [6] knowledge-compilation, [4] software-model checking, [15,16] software testing, [17] package management in software distributions, [18] checking of pedigree consistency, [19] verification of pipelined processors, [20–21] symbolic-trajectory evaluation, [22] test-pattern generation in digital systems, [23] design debugging and diagnosis, [10] identification of functional dependencies in Boolean functions, [24] technology-mapping in logic synthesis, [25] circuit-delay computation, [26] and cross-talk-noise prediction. [5] However, this list is incomplete, as the number of applications of SAT has been on the rise in recent years. [18,19,24]

Besides practical applications, SAT has also influenced a number of related decision and optimization problems, which will be referred to as extensions of SAT. Most extensions of SAT either use the same algorithmic techniques as used in SAT, or use SAT as a core engine.