O'Reilly logo

Verification Techniques for System-Level Design by Mukul Prasad, Indradeep Ghosh, Masahiro Fujita

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required