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.

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.

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.

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.

Abstract Reasoning

1. #SAT(F)=0 if and only if F is unsatisfiable; thus an exact #SAT oracle decides SAT by testing positivity. 2. A tautology over n counted variables has 2^n satisfying assignments. 3. Adding a logically redundant clause leaves the count unchanged, while adding a genuine constraint can only weakly decrease it. 4. Introducing an unconstrained counted variable doubles the count; introducing a uniquely determined auxiliary variable preserves it.

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.

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

• Algebraic Decision Diagram — 0.78
• Switching lemma — 0.78
• Fuzzy rule — 0.77
• MAX-3SAT — 0.77
• Functional completeness — 0.77

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