Skip to content

Satisfiability

A formal formula or jointly interpreted set is satisfiable when at least one permitted interpretation makes it true.

Version
v1 · 2026-10-17 · History
Domain-specific #
14283
Domain group
Formal Sciences
Origin domain
Mathematics
Subdomains
Formal Semantics, Satisfiability → Mathematics
Aliases
Satisfiability problem

Core Idea

A formula is satisfiable if at least one interpretation permitted by its formal logic makes it true. A set of formulas is jointly satisfiable if one interpretation makes every member true. For a finite set, this can be expressed by the conjunction of its members; the semantic condition also applies to sets not presented as one finite conjunction. The interpretation must obey any declared background theory. Without a qualifying interpretation, the formula or set is unsatisfiable.[1][2]

The satisfiability problem asks whether that model-existence condition holds. Propositional SAT searches Boolean valuations; satisfiability modulo theories (SMT) restricts interpretations using theories such as arithmetic or arrays. The semantic property exists independently of the method used to decide it. A displayed model can witness a positive answer, but no model printout is required for satisfiability to hold.[1][2]

Structural Signature

  • Formula or jointly asserted set. There must be a formal truth condition. For a set, the same interpretation must satisfy every member; separate models for separate members do not establish joint satisfiability.[1]
  • Declared language and semantics. Sorts, symbols, logical operations, and satisfaction rules determine what the expressions mean. Boolean clauses and array select/store formulas do not use the same semantic carrier.[3][4]
  • Admissible interpretations. The model space is fixed by the logic and, when present, a background theory. A theory constrains how some symbols may be interpreted; a separate theory is not mandatory in a purely propositional example.[1]
  • Satisfaction test. A proposed interpretation must make the formula true, or all asserted formulas true together. Merely assigning values to symbols is insufficient if a constraint fails.[1][2]
  • Existential model condition. One permitted satisfying interpretation is enough. Requiring truth under every interpretation asks about validity instead.[3]
  • Optional decision and witness output. A solver can report sat, unsat, or unknown; a model can be retrieved after a positive result in Z3. unknown means the run settled neither side, while satisfiability remains a definite semantic question.[2]

The first five roles define the property. The last role explains how the property is queried or evidenced without treating a particular solver response as part of the formula's identity.

What It Is Not

Not validity or tautology. A satisfiable formula may be true in one interpretation and false in another. Validity requires truth in every admissible interpretation. Under matched semantics, a formula is valid exactly when its negation is unsatisfiable.[3]

Not an interpretation by itself. An interpretation assigns meanings or values; satisfiability claims that at least one such assignment satisfies a specified formula. An array value without a formula to test is not a satisfiability instance.[1][4]

Not equisatisfiability. That relation compares two formulas and asks whether they share the same existence-of-a-model status. Not MaxSAT. Maximum satisfiability optimizes how many Boolean clauses can be satisfied, including cases where all cannot hold together. Ordinary satisfiability asks whether every asserted clause has a common model.

Scope of Application

The definition travels among formal logics that specify formulas, satisfaction, and admissible interpretations. For Boolean formulas, interpretations assign truth values to propositions. In SMT, a background theory can fix meanings for arithmetic, arrays, equality, or other symbols; a satisfying interpretation must respect those constraints.[3][1]

Barrett and Tinelli describe SAT and SMT as tools used in hardware and software verification, model checking, testing, and related work.[1] Those applications encode questions as formulas, but no one application is needed to define satisfiability. The difficulty of deciding the property and the solver's ability to return a model depend on the selected logic, fragment, and procedure. A solver's unknown is an operational limit, not a third semantic truth value for the formula.[2][1]

Clarity

Ask which interpretations are allowed before asking whether a formula is satisfiable. The array example below uses read/write axioms and an equality condition; stripping those semantics and looking only at its Boolean skeleton would answer a different question.[4][1]

Also separate a witness from a decision. Exhibiting one model proves satisfiability. A sound unsat result says no permitted model exists, while a solver's unknown leaves the decision unanswered. The latter does not mean “neither satisfiable nor unsatisfiable.”[2]

Manages Complexity

The existential test compresses many possible assignments or structures into a precise yes/no question: is there a common model? A solver may search valuations, reason under a background theory, or combine those methods. The model-existence target remains the same even when the procedure changes.[1]

That compression does not eliminate the formal context. If the formula, sorts, or background theory change, the space of admissible models can change. To compare two solver runs, hold those inputs fixed or state the transformation that relates them. A faster or more elaborate solver is not itself a new meaning of satisfiability.[1]

Abstract Reasoning

Fix the formula or set and its formal semantics. Specify any theory restricting interpretations. Ask whether some admissible interpretation satisfies the whole condition. If one exists, the condition is satisfiable; if none exists, it is unsatisfiable. A procedure may certify either answer, display a model, or fail to decide the case.[1][2]

For validity, negate the target formula and test the negation for satisfiability under the same semantics. If the negation has no model, the original is valid. This duality is a useful reasoning move, but it does not collapse the two properties into one: “some” and “all” still ask different questions.[3]

Knowledge Transfer

Literal transfer occurs from Boolean constraints to theory-constrained formulas because both retain a formal object, satisfaction relation, admissible model space, and existential test. The valuation or structure that counts as a model changes, so a Boolean witness cannot be copied into an integer-array problem. The Z3 Boolean and array cases below demonstrate the shared question with unlike carriers.[5][4]

The word “satisfiable” sometimes appears in ordinary planning or preference talk. Those uses are analogies unless the constraints, interpretations, and satisfaction rule have actually been formalized. Applying the SAT label to a vague feasible plan without a declared semantics would borrow vocabulary rather than transfer this precise property.

Examples

Boolean clauses about Tie and Shirt

The solver-authored Programming Z3 tutorial asserts three formulas built from Boolean Tie and Shirt variables. Z3 reports sat and displays Tie=false, Shirt=true as one assignment making the asserted set true.[5] The displayed assignment proves existence; it is not a requirement that every satisfying valuation be listed.

Mapped back: the three clauses are the formal object, Boolean connectives give their semantics, Boolean valuations are the permitted interpretations, each clause must evaluate true under one valuation, and the displayed assignment witnesses the existential condition. This is a didactic propositional case, not evidence for any particular hardware-verification trace.

Integer-array select/store constraints

The official Z3 Arrays guide considers an integer array a1 with constraints (select a1 x)=x and (store a1 x y)=a1. It says they are satisfiable when x=y and an appropriate array maps x to itself. Adding x≠y makes the set unsatisfiable under the guide's array semantics.[4] These are claims about that example and its stated theory, not a universal result for every array extension.

Mapped back: the two original equations and optional disequality are the asserted formulas; select/store and array equality determine their semantics; admissible interpretations assign integer values and an array respecting that theory; the base conditions have a common model, while the strengthened conditions do not. The guide does not require a full array model to be printed for this distinction to hold.

Structural Tensions

No intrinsic opposed-pressure tradeoff defines the satisfiability property. Barrett and Tinelli discuss how richer logics can make automated decision more difficult, but that concerns the chosen representation and procedure; it does not alter the underlying existence condition.[1]

Structural–Framed Character

Satisfiability is structural within formal semantics: the existential model test survives changes from Boolean valuations to theory-constrained structures. Its evaluative weight is conditional: a satisfiable specification may contain an error, and an unsatisfiable specification may intentionally describe an impossible state. Human-practice dependence lies in selecting the language, theory, and encoded question; after those are fixed, the property follows from the semantics. Its institutional origin is mathematical logic and automated reasoning rather than a specific solver vendor. Its vocabulary travels literally across formal languages with defined satisfaction and only analogically into loosely stated practical goals. For import versus recognition, a new case qualifies by an actual model-existence question, not by the presence of constraints alone. Its character: a formal semantic property with a related decision problem and optional witness output.

Structural Core vs. Domain Accent

The broad shape is “some admissible state meets a condition.” The domain-bound mechanism is precise: formal expressions are evaluated under a declared satisfaction relation over permitted interpretations, possibly restricted by a theory. Removing that semantics leaves a generic feasibility intuition rather than logical satisfiability.

Consistency is a broader Prime about jointly possible commitments; its binding-commitment and conflict-localization roles do not make this exact formula-level model-existence property a duplicate. A logical interpretation supplies possible assignments, Tautology (Logic) requires all valuations, and Equisatisfiability compares two formulas' existence statuses. The formal property retains a specific semantic residual beyond those neighbors.

Future-Prime question: Would two independently sourced, nonformal domains support the same necessary roles—including a declared interpretation class and truth rule—without merely encoding their problems into logic? That evidence could motivate a broader abstraction; the current sources establish formal transfer across Boolean and theory-based logics.

Consistency is a conceptual neighbor because joint satisfiability often tests whether formal commitments can hold together. Its live description also reaches law, narratives, and personal commitments, with binding-commitment and conflict-localization roles absent from this formula-level property. A positive model is an interpretation or valuation satisfying the given formula; satisfiability is the existence claim, not the assignment object.

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

Computed from structural-signature embeddings · 2026-10-17

Not to Be Confused With

  • Validity / tautology: truth under all permitted interpretations; a satisfiable formula needs only one.[3]
  • A particular witness model: useful proof of sat, but not a required report.[2]
  • A solver answer of unknown: inability of that run to decide, not semantic unsatisfiability.[2]
  • Equisatisfiability: same satisfiable/unsatisfiable status for two formulas, possibly with different model sets.
  • Maximum satisfiability: optimization of a Boolean clause objective, not a common model for all asserted clauses.

References

[1] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n

[2] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i

[3] Z3 Team, “Propositional Logic,” Online Z3 Guide, §Satisfiability and Validity. https://microsoft.github.io/z3guide/docs/logic/propositional-logic/ . Official full HTML inspected. registry ↩a ↩b ↩c ↩d ↩e ↩f

[4] Z3 Team, “Arrays,” Online Z3 Guide, introduction and §Select and Store. https://microsoft.github.io/z3guide/docs/theories/Arrays/ . Official full HTML inspected. registry ↩a ↩b ↩c ↩d ↩e

[5] 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. registry ↩a ↩b