As society relies more and more on increasingly complex computational systems, the need for verifying the correctness of computer hardware and software, especially in safety-critical applications, has grown rapidly. Even in a computer chip that is not used in safety-critical applications, it is important to verify that its design is correct to avoid the enormous cost of withdrawing an incorrect design from the market and re-implementing it. In the early Intel Pentium processors, the so-called FDIV bug in the hardware of its floating point unit sometimes caused the processor to compute the wrong answer when dividing two floating point numbers. This bug caused Intel to recall the defective processors and take a US$475 million charge against earnings in 1994. Although simulating a design in software can catch some bugs, testing all possible inputs for faulty outputs creates a space of possible behaviors simply too large to search exhaustively, as shown by the FDIV bug. As a result, Intel and other hardware providers subsequently invested heavily in building groups that developed formal verification techniques that are useful to prove properties of hardware.

The development of solvers for the propositional satisfiability problem (SAT) has attracted very significant resources over the last few decades. Although SAT may be worst-case exponential, instances that occur in real applications, with millions of variables, can now be realistically solved. Some approaches to proving hardware and software correctness can exploit the progress in SAT solver performance. One method for doing that is to specify the range of desired behaviors of a system in terms of a logical formula constraining the system’s inputs and outputs. Given a description of the design of the system, the problem then is to determine that the design always satisfies its formal specification. A technique known as bounded model checking (BMC) is widely used for hardware verification. BMC represents a bounded-length execution trace that would violate a required property. Each execution trace symbolically represents a large set of possible actual traces, thereby overcoming the difficulty of verifying the system by simulation on all possible inputs. The propositional formula that results is tested with a SAT solver. If the formula can be satisfied then the trace is feasible and the property has been violated. If not, then the bound is increased, repeating the process. BMC has also been applied to software verification, in a similar way, with some success. An alternative approach to the formal specification and verification of software and hardware systems is the TLA$+$ system, based on extensions to logic that include time (known as temporal logic).

SAT has many other significant industrial applications. One family of such applications is product configuration. A product line, such as a line of cars, is a family of similar products. Various features are available to be reused across the family. A product’s configuration is the set of features it uses. A feature model characterizes the allowable configurations, specifying the constraints among the features that are used. A feature model, combined with user-supplied constraints, can be translated to a SAT formula to enumerate the set of acceptable legal configurations with a SAT solver. Formal methods were applied to the task of managing all possible configurations of the Mercedes lines of passenger cars and commercial vehicles. SAT solving was applied to the task of maintaining consistency in the database of thousands of logical constraints, and keeping it consistent as it constantly changes with the phasing in and out of models and parts.

Other important SAT applications include planning and scheduling for shift workers, sports tournaments, exams, and air traffic control.