Overview

Boolean Satisfiability, abbreviated SAT, is the problem of deciding whether a Boolean formula admits an assignment that makes it evaluate to true. In the provided evidence, SAT appears in three main roles: (1) as the solving engine at the core of SAT-based formal hardware verification techniques, (2) as the foundation for SAT-related extensions such as uniform witness generation and model counting, and (3) as the conceptual origin of related problems such as unsatisfiable-core and minimal unsatisfiable subformula computation, which are reused in adjacent domains such as diagnosing over-constrained constraint-based random simulation.[C1][C2][C3][C4][C8]

Use in formal hardware verification

SAT-based methods are described as a robust solution in formal verification. SAT-based Bounded Model Checking (BMC) is identified as a prominent technique whose performance improvements have made it suitable for larger-scale designs.[C1]

In the described verification setting, the intended behavior of a design is formalized using safety properties. Restricting checking to safety properties leads to bounded properties that can be checked efficiently using a SAT solver.[C3]

A synchronous circuit is modeled as a finite-state machine with inputs, outputs, states, initial states, an output function, and a next-state function. Its transition relation can be written as:

T(s, s') = exists x in B^n : s' == Delta(x, s)

A safety property f = AG(phi) is translated into a Boolean function [[f]]_t that checks the validity of phi at a time point t. The translation is constructed so that a satisfying assignment of [[f]]_t corresponds to a counterexample of phi.[C4]

SAT instances in interval property checking

Interval property checking (IPC) searches for counterexamples by solving a SAT instance that combines an unrolled transition relation with the Boolean encoding of the property. In the provided formalization, the transition relation is unrolled over a bounded interval and connected to a single instantiation of the translated property:

AND_{i=0..c} T(s_{t+i}, s_{t+i+1}) AND [[f]]_t

The result is a SAT problem whose satisfying assignments indicate counterexamples for the checked safety property.[C5]

Relationship to BMC and IPC

SAT-based BMC is presented as one of the prominent SAT-based formal verification techniques. IPC is contrasted with original BMC: IPC verifies only safety properties and uses an arbitrary starting state rather than the initial state used in BMC. A property that holds from an arbitrary state also holds from any reachable state, giving exhaustive verification under that condition.[C6]

Because IPC can start from unreachable states, it can produce false negatives: counterexamples that arise only from unreachable states. The evidence states that such false negatives must be removed by adding invariants that restrict the starting state.[C6]

SAT with additional constraints: the transitivity example

SAT is also used as the backbone for problems in which the formula is augmented with structured side constraints. In one setting, a subset of the variables of a formula Fsat encodes a symmetric, transitive, binary relation over N elements through variables e[i,j] for 1 <= i < j <= N, expressing whether the relation holds between i and j. The task is to either find a satisfying assignment of Fsat that also satisfies all transitivity constraints (e.g., e[1,2] & e[2,3] ==> e[1,3]), or prove that no such assignment exists. To use a conventional Boolean satisfiability checker, the set of clauses expressing Fsat is augmented with clauses expressing the transitivity constraints, and reductions exploit the sparse structure of the relational variables.[C2]

SAT notation and witness terminology

In modern SAT treatments, formulas are assumed to be in conjunctive normal form (CNF). Given a Boolean formula F in CNF, the set X of variables appearing in F is called the support of F. A satisfying assignment or witness of F is an assignment of truth values to variables in its support such that F evaluates to true. The set of all witnesses is denoted R_F. A subset D of X is called a dependent support of F if no two satisfying assignments of F differ only in the truth values of variables in D; the complement X \ D is called an independent support of F. A formula may have more than one independent support, and every superset of an independent support is again an independent support. For example, (a v ¬b) ∧ (¬a v b) has three independent supports: {a}, {b}, and {a, b}.[C8]

Beyond decision: uniform witness generation and model counting

Beyond the classical decision problem, SAT also underlies two problems that have attracted significant theoretical and practical interest:

• Uniform witness generation: producing a satisfying assignment chosen uniformly at random from R_F. A uniform generator G^u is a probabilistic algorithm guaranteeing Pr[G^u(F) = y] = 1/|R_F| for every y in R_F. An almost-uniform generator G^au provides a two-sided multiplicative tolerance: for every y in R_F, 1 / ((1 + ε) |R_F|) <= Pr[G^au(F, ε) = y] <= (1 + ε) / |R_F|, where ε > 0 is the specified tolerance.[C8]

• Model counting: determining the total number of satisfying assignments |R_F|. The combination of uniform generation and counting gives rise to approximate model counters.[C3]

Prior work on these problems offered either heuristic approaches with weak or no performance guarantees or theoretical approaches with proven guarantees but poor practical performance. A limited-independence-hashing-based approach designs algorithms for both problems with strong theoretical guarantees and scalability extending to thousands of variables, yielding practical algorithms such as UniformWitness (a near-uniform generator) and approxMC (a scalable approximate model counter), both of which work by issuing polynomial calls to a SAT solver.[C3]

Earlier SAT-based witness-generation algorithms include PAWS (Sabharwal and Selman), designed to work with any discrete distribution specified through a graphical model and applicable to uniform generation when restricted to distributions that assign equal weight to every assignment, and UniWit. Both algorithms have inherent limitations that make it difficult to scale them to Boolean constraints with tens of thousands of variables and beyond, and provide guarantees that are weaker than what one would desire in practice. They were followed by UniGen, which is the first algorithm to provide strong two-sided guarantees of almost-uniformity while scaling to problems involving hundreds of thousands of variables, and which significantly improves the success probability both in theory and in experiments.[C8]

Related problems: unsatisfiable cores and minimal unsatisfiable subformulas

In the SAT domain, the evidence identifies an analogous sub-problem to diagnosing over-constrained constraint satisfaction problems: computing an unsatisfiable core of an unsatisfiable formula, i.e. identifying an unsatisfiable sub-formula of the overall formula. To obtain a minimal reason for the unsatisfiability, the more complex problem of a minimal unsat core (a minimal unsatisfiable sub-formula) must be considered. Furthermore, all minimal unsat cores are required to determine all contradictions, which is in general very time consuming.[C7]

Practical significance

Within the evidence, SAT is not treated as an isolated topic but as an enabling mechanism for formal verification workflows, for richer algorithmic tasks such as uniform witness generation and model counting, and for diagnosing contradictions in constraint-based settings. SAT solvers are used to efficiently check bounded safety properties; SAT instances encode both the transition behavior of a design and the condition whose satisfaction corresponds to a counterexample; SAT calls power polynomial-time reduction steps in witness-generation and model-counting algorithms; and SAT sub-problems (unsat cores and minimal unsatisfiable subformulas) are the natural counterparts of contradiction analysis in over-constrained constraint systems.[C3][C5][C7][C8]