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