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 the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
