Satisfiability¶
A formal formula or jointly interpreted set is satisfiable when at least one permitted interpretation makes it true.
Core Idea¶
A formal formula is satisfiable when at least one interpretation permitted by its logic makes it true. A set of formulas is jointly satisfiable when one interpretation makes every member true. The satisfiability problem asks whether that model exists; a solver may display a witness, but the property does not depend on a printout. For a finite set, one can instead test the conjunction of its members. Changing the permitted interpretations can change the answer even with the same written formula.[ref-47585d7f7d7b][ref-17281bb5b5ee]
Scope of Application¶
The test travels literally among formal languages with declared formulas, satisfaction rules, and admissible interpretations.
- Propositional SAT: ask whether some Boolean assignment makes every asserted clause true.[^ref-90c41ce0f8a6]
- SMT: ask the same question while respecting a background theory's restrictions on interpretations.[^ref-47585d7f7d7b]
- Boolean solver example: Z3's Tie/Shirt clauses have a common model, with Tie false and Shirt true.[^ref-88b488f5c5ab]
- Array constraints: read/write semantics admit a model when the example's indices are equal; adding their inequality makes the set unsatisfiable.[^ref-8544602b69e9]
- Verification encodings: hardware or software questions can be encoded as formulas whose model-existence status is tested.[^ref-47585d7f7d7b]
Clarity¶
Satisfiability asks whether a common model exists, not whether a formula is true under every interpretation; that stronger condition is validity. It also differs from an interpretation alone, which supplies possible meanings without a target formula, and from equisatisfiability, which compares two formulas' statuses. A solver's unknown says that run decided neither side; it is not a third semantic status.[ref-90c41ce0f8a6][ref-17281bb5b5ee]
Manages Complexity¶
The property compresses a potentially large space of assignments or structures into one yes/no question. Solvers may search Boolean valuations or reason under array and arithmetic theories, but the formal target stays the existence of one model satisfying the whole condition. The compression depends on the declared language and theory: changing either can change which interpretations count, so results from different encodings cannot simply be interchanged.[^ref-47585d7f7d7b]
Abstract Reasoning¶
Fix the formula or jointly asserted set, its semantics, and any background theory; then test whether some admissible interpretation satisfies all of it. A found model proves satisfiability, while a justified unsatisfiable result excludes every permitted model. To test validity under matching semantics, ask whether the formula's negation is unsatisfiable. Keep that all-model question distinct from satisfiability's some-model question.[ref-90c41ce0f8a6][ref-17281bb5b5ee]
Knowledge Transfer¶
The same existential model test works for Boolean valuations and theory-constrained array structures, although their witnesses have different forms.[ref-47585d7f7d7b][ref-8544602b69e9] Transfer the question by mapping the formula, semantics, interpretation class, satisfaction rule, and existential condition in the new logic; do not carry a Boolean valuation into an array model. A changed background theory can alter which models count, so repeat the existence test under the new rules.[^ref-47585d7f7d7b] Outside a declared formal semantics, calling a practical plan “satisfiable” is only an analogy.
Neighborhood in Abstraction Space¶
Satisfiability sits in a sparse region of the domain-specific corpus (73rd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Logical Semantics & Many-Valued Systems (12 abstractions)
Nearest neighbors
- Equisatisfiability — 0.84
- Positive set theory — 0.84
- Indiscernibles — 0.83
- Monadic predicate calculus — 0.83
- Finite-Valued Logic — 0.83
Computed from structural-signature embeddings · 2026-10-17
References¶
[^ref-47585d7f7d7b]: Clark Barrett and Cesare Tinelli, “Satisfiability Modulo Theories,” in Handbook of Model Checking (Springer, 2018), especially §1.1 and pp.4–5 of the full chapter PDF. https://theory.stanford.edu/~barrett/pubs/BT18.pdf . Authoritative full chapter inspected; provides T-satisfiability and context for propositional abstraction and applications.
[^ref-88b488f5c5ab]: Nikolaj Bjørner, Leonardo de Moura, Lev Nachmanson, and Christoph Wintersteiger, “Programming Z3,” §2, “Logical Interfaces to Z3.” https://theory.stanford.edu/~nikolaj/programmingz3.html . Original solver-author tutorial; full search-indexed text inspected for the Tie/Shirt example, but direct live HTML fetching timed out.
[^ref-90c41ce0f8a6]: Z3 Team, “Propositional Logic,” Online Z3 Guide, §Satisfiability and Validity. https://microsoft.github.io/z3guide/docs/logic/propositional-logic/ . Official full HTML inspected.
[^ref-8544602b69e9]: Z3 Team, “Arrays,” Online Z3 Guide, introduction and §Select and Store. https://microsoft.github.io/z3guide/docs/theories/Arrays/ . Official full HTML inspected.
[^ref-17281bb5b5ee]: Z3 Team, “Basic Commands,” Online Z3 Guide, check-sat and get-model discussion. https://microsoft.github.io/z3guide/docs/logic/basiccommands/ . Official full HTML inspected.