Chapter 3. Basic Technology for Formal Verification

The Boolean Satisfiability Problem

The Boolean satisfiability (SAT) problem is a well-known constraint satisfaction problem, with many applications in the fields of VLSI computer-aided design and artificial intelligence. Given a propositional formula ϕ, the Boolean satisfiability problem posed on ϕ is to determine if there exists a variable assignment under which ϕ evaluates to true. Such an assignment, if one exists, is called a satisfying assignment for ϕ, and ϕ is called satisfiable. Otherwise, ϕ is said to be unsatisfiable. The SAT problem is known to be NP-complete [1]. However, in recent years, there have been tremendous advancements in SAT technology, making SAT solvers a viable option ...

Get Verification Techniques for System-Level Design now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.