Sharp Satisfiability (#SAT)¶

The counting problem that maps a Boolean formula to the exact number of truth assignments satisfying it, refining SAT's yes/no question into a model count.

Version: v1 · 2026-08-30 · History
Domain-specific #: 2768
Origin domain: computer science
Subdomain: computational complexity
Aliases: #SAT, ♯SAT, Sharp SAT, Boolean model counting

Core Idea¶

Sharp Satisfiability, written #SAT or ♯SAT, maps a Boolean formula to the number of truth assignments under which the formula evaluates to true. SAT asks whether this number is positive. #SAT asks for the integer itself. For a formula on n variables, the output lies between 0 and 2^n; it distinguishes unsatisfiable formulas, uniquely satisfiable formulas, and formulas with many models even though SAT returns only “no” or “yes.”

The problem is a canonical complete problem for the counting complexity class #P. A #P function counts accepting computation paths of a nondeterministic polynomial-time machine; satisfying assignments play that role for a Boolean verifier. Reductions must be specified carefully because an ordinary many-one reduction preserving only yes/no satisfiability need not preserve the number of solutions. Parsimonious reductions preserve counts exactly; Turing and metric reductions support other completeness results but license different inferences.^[1]

The locked identity is: finite Boolean formula over a declared variable set + all total truth assignments + standard Boolean evaluation -> exact cardinality of the satisfying-assignment set. The output is a nonnegative integer, not a witness, probability, or approximation. Algorithms may avoid explicit enumeration, but the semantic target remains the full exact count.

Structural Signature¶

the Boolean formula F — expression in a declared syntax such as CNF, DNF, or circuit representation;
the variable set Var(F) — variables over which assignments are counted, including any explicitly declared free variables;
the assignment space — all maps from the counted variables to {false,true};
the satisfaction predicate — deterministic evaluation deciding whether one assignment makes F true;
the model set — {a : F(a)=true};
the cardinality output — #SAT(F)=|{a:F(a)=true}|;
the representation class — unrestricted CNF, k-CNF, Horn, monotone, bounded-treewidth, or another family affecting complexity;
the reduction notion — parsimonious, many-one, Turing, or approximation-preserving, stated with the theorem;
the computational method — branching, dynamic programming, knowledge compilation, inclusion–exclusion, or another exact counter;
the decomposition/cache state — repeated residual formulas reused rather than recounted;
the numeric representation — enough bits to express a count up to 2^n;
the correctness obligation — every satisfying assignment counted once and every nonsatisfying assignment excluded.

Recognition requires an exact count of satisfying total assignments. Merely finding, sampling, or deciding models does not satisfy the identity.

What It Is Not¶

Not SAT. SAT returns whether at least one model exists.
Not a satisfying assignment. A witness is one model, while #SAT returns how many models there are.
Not enumeration output. Listing every model can compute the count, but #SAT's required output is the number.
Not approximate model counting. An interval or probabilistic estimate is a different task unless exactness is explicitly recovered.
Not weighted model counting. Weighted counting sums weights over models rather than assigning weight one to every model.
Not Max-SAT. Max-SAT optimizes the number or weight of satisfied clauses under one assignment.
Not probability by itself. Under the uniform distribution, dividing by 2^n yields a satisfaction probability; #SAT itself is the numerator.
Not automatically hard for every restricted syntax. Formula structure can create polynomial-time subclasses.
Not Bloom Filter. The catalog's semantic retrieval neighbor is an approximate membership data structure with false positives, not a Boolean model count.

Scope of Application¶

SAT anchors counting complexity and exact propositional model counting. It appears in formal verification, probabilistic inference, reliability, planning, database query evaluation, cryptographic analysis, combinatorics, and artificial intelligence. If a domain can encode its valid configurations as satisfying assignments, #SAT provides their cardinality. The encoding and reduction determine whether the resulting count corresponds one-to-one with original objects or includes auxiliary multiplicity.¶

Restricted formula classes expose an important boundary between decision and counting complexity. A decision problem can be tractable while its counting analogue remains hard because existence can ignore multiplicity. Conversely, structural restrictions such as bounded treewidth, decomposable compiled forms, or affine constraints can permit efficient exact counting. It is therefore unsafe to infer #SAT complexity merely from the complexity of SAT on the same syntax.

Modern exact solvers often extend DPLL/CDCL-style search with component decomposition, clause learning, caching, and arithmetic aggregation. Knowledge-compilation approaches transform formulas into representations such as deterministic decomposable negation normal form, where model count can be computed compositionally. These are methods for the same abstraction; no particular algorithm defines #SAT.

Clarity¶

Suppose F=(x∨y)∧(¬x∨y). Of four assignments to x,y, exactly the two with y=true satisfy F, so #SAT(F)=2. SAT discards the difference between this formula and one with a unique model. #SAT preserves it.

Declared variables matter. A formula containing only x has one satisfying assignment over {x} if it forces x=true; if the counting universe is declared as {x,y}, the unconstrained y doubles the model count. Implementations must state whether variables absent after simplification remain in the original universe. Auxiliary variables introduced by an encoding can similarly change counts unless extensions are unique or the reduction accounts for multiplicity.

prime:complete_enumeration supplies exhaustive coverage of a finite possibility space. #SAT can instantiate that logic semantically even when an algorithm counts without listing. The prime does not provide Boolean syntax, satisfaction, #P classification, reduction conditions, or model-counting algorithms, so exact coverage is absent.

Manages Complexity¶

Counting compresses an exponentially large solution set into an integer while retaining information that existence loses. It enables comparisons of constraint strength, probabilities under uniform assignments, numbers of valid configurations, and quantitative confidence in verification claims. The integer may require only O(n) bits even when the represented model set has exponential size.

The computational difficulty remains: compression of output does not guarantee cheap computation. Decomposition manages this difficulty by exploiting independent variable components. If F=G∧H and G,H have disjoint variable sets, counts multiply. For deterministic alternatives whose model sets are disjoint, counts add. Caching prevents repeated counting of identical residual subproblems. These algebraic rules explain why compilation and structural width can turn impossible brute-force enumeration into tractable exact arithmetic.

Abstract Reasoning¶

#SAT(F)=0 if and only if F is unsatisfiable; thus an exact #SAT oracle decides SAT by testing positivity.
A tautology over n counted variables has 2^n satisfying assignments.
Adding a logically redundant clause leaves the count unchanged, while adding a genuine constraint can only weakly decrease it.
Introducing an unconstrained counted variable doubles the count; introducing a uniquely determined auxiliary variable preserves it.
For independent conjuncts on disjoint variable sets, counts multiply; overlapping variables invalidate naive multiplication.
For disjoint model sets, disjunctive counts add; without disjointness, overlap must be subtracted or structurally eliminated.
A reduction preserving satisfiability but mapping each source model to several target models cannot be used as a parsimonious counting proof.
Uniform satisfaction probability equals #SAT(F)/2^n, provided the denominator uses exactly the counted variable set.
Approximate counters can be useful at large scale but do not establish an exact integer unless their guarantee degenerates to certainty and zero error.
A compact knowledge representation supports efficient counting only when its decomposition/determinism properties match the counting operations.

Knowledge Transfer¶

Exact transfer occurs from propositional formulas to encoded finite configuration problems when the encoding is count-preserving or its multiplicity is corrected. Examples include counting graph colorings, schedules, diagnoses, circuit inputs, or database assignments encoded in Boolean variables. The problem's roles remain formula, assignment universe, predicate, and cardinality.

Weighted model counting generalizes #SAT by replacing unit weight with assignment or literal weights; algebraic model counting generalizes addition and multiplication further. These are related abstractions, not aliases, because their codomain and aggregation semantics differ. The prime-level portable residue is counting a predicate-defined finite set.

Examples¶

unique model: x∧y has count one over {x,y}.
tautology: x∨¬x has count two over {x}.
unsatisfiable formula: x∧¬x has count zero.
independent components: if G has three models and H has five on disjoint variables, G∧H has fifteen.
network reliability encoding: assignments represent component up/down states and the formula represents connectivity; #SAT counts working states before weights are introduced.
formal verification: a formula encoding counterexamples can be counted to distinguish one rare failure from a broad failure region.
non-example: a SAT solver returning one witness does not compute #SAT.

Structural Tensions¶

semantic simplicity vs. computational hardness — the definition is a cardinality, but exact computation can be #P-complete;
encoding convenience vs. count preservation — auxiliary variables simplify clauses while risking multiplicity distortion;
exactness vs. scalability — exact counts support hard guarantees, whereas approximation reaches larger instances;
decomposition vs. coupling — independent components multiply cleanly, but shared variables destroy factorization;
representation size vs. query speed — compilation may be expensive or large but enables repeated rapid counts.

Structural–Framed Character¶

SAT is structural. Boolean semantics and cardinality determine the output independently of institutions or interpretive communities. The sharp sign, syntax conventions, and named complexity classes are framed labels, but the underlying function and proofs are mathematical.¶

Structural Core vs. Domain Accent¶

The core is finite candidate space + predicate -> number of satisfying candidates. The domain accent is Boolean formulas, truth assignments, propositional satisfaction, and #P reductions. Removing it yields generic Counting or Complete Enumeration rather than #SAT.

Complete Enumeration — the semantic count covers the entire assignment universe, even if computation is symbolic.
Compression — exponentially many models are represented by a binary integer.
Decomposition — independent subformulas support multiplicative counting.
Constraint — clauses carve the model set from all possible assignments.

The prospective DAG uses composition under prime:complete_enumeration.

Relationships to Other Abstractions¶

Current abstraction Sharp Satisfiability (#SAT) Domain-specific

Parents (1) — more general patterns this builds on

Sharp Satisfiability (#SAT) is part of Complete Enumeration Prime

the semantic count covers the entire assignment universe, even if computation is symbolic.

Hierarchy path (1) — routes to 1 parentless root

Sharp Satisfiability (#SAT) → Complete Enumeration → Completeness

Neighborhood in Abstraction Space¶

Sharp Satisfiability (#SAT) sits in a sparse region of the domain-specific corpus (93^rd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

SAT or Unique-SAT;
Max-SAT;
model enumeration;
approximate model counting;
weighted model counting;
counting accepting paths without a specified reduction to Boolean models;
a decision-complexity result transferred without checking reduction type.

References¶

[1] Leslie G. Valiant, “The Complexity of Enumeration and Reliability Problems,” SIAM Journal on Computing 8(3), 1979, 410–421, https://doi.org/10.1137/0208032. registry ↩

[2] Christos H. Papadimitriou, Computational Complexity, Addison-Wesley, 1994, chapters on counting complexity. registry

[3] Adnan Darwiche, “New Advances in Compiling CNF to Decomposable Negation Normal Form,” ECAI 2004, and related knowledge-compilation literature. registry

[4] “♯SAT,” Wikipedia, frozen evidence packet, https://en.wikipedia.org/wiki/%E2%99%AFSAT. registry