Boolean Satisfiability

Concept

Boolean Satisfiability (SAT) is the decision problem of determining whether a Boolean formula admits a satisfying assignment. In the provided evidence SAT is treated both as the solving engine behind formal hardware verification techniques such as SAT-based Bounded Model Checking and Interval Property Checking, and as the foundation for richer SAT-related problems including uniform witness generation, model counting, and the computation of unsatisfiable cores and minimal unsatisfiable subformulas.

First seen 5/26/2026

Last seen 7/26/2026

Evidence 5 chunks

Wiki v3

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

6 connections

Interval Property Checking ← uses 100% 3e

IPC uses SAT-based methods for verification.

Bounded Model Checking ← uses 100% 1e

Bounded model checking uses Boolean satisfiability (SAT) as its core solving mechanism.

Contradiction Analysis for Constraint-based Random Simulation ← mentions 90% 1e

The paper mentions Boolean Satisfiability as an analogous domain where unsat core computation is performed.

Minimal Unsatisfiable Subformula ← derived from 90% 1e

Minimal unsatisfiable subformulas are a concept arising in the Boolean satisfiability domain.

constrained random verification ← uses 95% 1e

CRV constraints are encoded as Boolean formulae for SAT-based witness generation.

CNF formula ← uses 92% 1e

CNF formulae are the input representation for Boolean satisfiability problems solved in this work.

LINKED ENTITIES

2 links

constrained random verification USES Extracted graph relationship

CNF formula USES Extracted graph relationship

CITATIONS

12 sources

12 citations — click to expand

[1] SAT plays a key role in diverse areas spanning testing, formal verification, planning, optimization, and inferencing. Sampling Techniques for Boolean Satisfiability

[2] A SAT-based decision procedure for a logic of equality with uninterpreted functions augments the clauses of Fsat with clauses expressing transitivity constraints over relational variables e[i,j]. Boolean Satisfiability with Transitivity Constraints

[3] SAT-based Bounded Model Checking (BMC) is identified as a prominent SAT-based formal verification technique whose performance improvements have made it suitable for larger-scale designs. Boolean Satisfiability

[4] Restricting verification to safety properties yields bounded properties that can be checked efficiently using a SAT solver. Boolean Satisfiability

[5] A synchronous circuit is modeled as a finite-state machine with transition relation T(s, s') = exists x in B^n : s' == Delta(x, s), and a safety property f = AG(phi) is translated into a Boolean function [[f]]_t whose satisfying assignments correspond to counterexamples. Boolean Satisfiability

[6] Interval property checking searches for counterexamples by solving the SAT instance AND_{i=0..c} T(s_{t+i}, s_{t+i+1}) AND [[f]]_t, whose satisfying assignments indicate counterexamples. Boolean Satisfiability

[7] IPC verifies only safety properties from an arbitrary starting state, giving exhaustive verification under that condition; because it can start from unreachable states it can produce false negatives, which are removed by adding invariants. Boolean Satisfiability

[8] Diagnosing over-constrained constraint satisfaction problems mirrors computing unsatisfiable cores; computing all minimal unsat cores is in general very time consuming. Boolean Satisfiability

[9] SAT problems are commonly expressed as CNF formulas; X is the support of F, a witness is an assignment that makes F evaluate to true, and a dependent support D is one in which no two witnesses differ only in variables from D, with X \ D called an independent support. Balancing Scalability and Uniformity in SAT Witness Generator

[10] A uniform generator G^u(F) guarantees Pr[G^u(F)=y] = 1/|R_F| for every y in R_F, while an almost-uniform generator G^au guarantees 1/((1+ε)|R_F|) <= Pr[G^au(F,ε)=y] <= (1+ε)/|R_F| for tolerance ε > 0. Balancing Scalability and Uniformity in SAT Witness Generator

[11] PAWS (Sabharwal and Selman) and UniWit are earlier SAT-based uniform witness generation algorithms that do not scale well beyond tens of thousands of variables and offer weaker guarantees; UniGen is the first algorithm to provide strong two-sided almost-uniformity guarantees while scaling to hundreds of thousands of variables. Balancing Scalability and Uniformity in SAT Witness Generator

[12] Limited-independence hashing yields SAT-based algorithms for uniform witness generation and approximate model counting with strong theoretical guarantees and scalability to thousands of variables, producing UniformWitness and approxMC, which work by issuing polynomial calls to a SAT solver. Sampling Techniques for Boolean Satisfiability