Equisatisfiability¶

The logical relation in which two formulas share the same existence-of-a-model status—both satisfiable or both unsatisfiable—without requiring the same models, enabling compact satisfiability-preserving transformations such as Tseitin encoding and Skolemization.

Version: v1 · 2026-08-30 · History
Domain-specific #: 1781
Origin domain: mathematical logic
Subdomain: satisfiability preserving transformations
Aliases: Equisatisfiable formulas, Satisfiability equivalence

Core Idea¶

Two logical formulas are equisatisfiable when either both have at least one model or neither has any model. Writing Sat(φ) for “there exists an interpretation or assignment satisfying φ,” the relation is φ ~sat ψ exactly when Sat(φ) <-> Sat(ψ). It preserves the answer to an existence question while allowing almost everything else about the formulas to change: syntax, vocabulary, number of variables, truth value under a particular assignment, and even the sets of models can differ.^[1]

The locked identity is two formulas interpreted under a declared satisfiability semantics + equality of their Boolean model-existence status -> permission to replace one with the other for a satisfiability decision. This weaker relation is computationally valuable. A transformation may introduce fresh variables and linear-size constraints instead of producing an equivalent formula whose normal form would grow exponentially. Tseitin encoding exemplifies this move: the encoded conjunctive-normal-form formula has a satisfying assignment if and only if the original formula does, although their signatures differ and they are not logically equivalent.^[2]^[3]

Equisatisfiability is a strict domain-specific specialization of Equivalence Relation: it is the kernel relation of the function Sat from formulas to the two-element set {satisfiable, unsatisfiable}. That observation does not make the candidate duplicate coverage. The logical specialization fixes the carrier, invariant, model-theoretic semantics, transformation obligations, witness-extension/restriction arguments, and solver use that the generic prime does not entail. It must remain distinct from logical equivalence, which preserves truth in every shared interpretation, and from mere one-way satisfiability preservation.

Structural Signature¶

a logic and semantics — propositional, first-order, modal, description, SMT, or another formal system with a declared satisfaction relation;
two well-formed formulas or theories — φ and ψ, possibly using different signatures when fresh symbols are admitted;
a model-existence predicate — Sat(χ) is true exactly when at least one permitted interpretation satisfies χ;
a bidirectional status condition — Sat(φ) implies Sat(ψ) and Sat(ψ) implies Sat(φ);
two equivalence classes — relative to the declared universe, formulas partition into satisfiable and unsatisfiable classes;
no same-model commitment — equisatisfiable formulas may disagree under particular assignments and need not share a signature;
a replacement purpose — typically deciding SAT/UNSAT, reducing a logic, or preparing input for an automated procedure;
a transformation — often a mapping T whose correctness claim is Sat(φ) <-> Sat(T(φ)) for every input in scope;
fresh-symbol discipline — auxiliary variables, constants, or functions must be new and their quantificational role controlled;
a forward witness map — a model of the source can be extended or translated to a model of the target;
a reverse witness map — a model of the target can be restricted or translated to demonstrate satisfiability of the source;
an unsatisfiability consequence — if one side is unsatisfiable, bidirectionality forces the other to be unsatisfiable;
a declared output requirement — SAT decision alone may be preserved even when model counting, validity, equivalence, or all-model enumeration are not;
a complexity payoff — weaker preservation may allow polynomial or linear representation where equivalence-preserving normalization expands;
a scope boundary — finite formulas, theories, signatures, and semantic classes must match the proof of preservation.

Merely mapping every satisfiable input to some satisfiable output is insufficient. The reverse implication is required, or spurious target models could turn an unsatisfiable source into a satisfiable encoding.

What It Is Not¶

Not logical equivalence. φ and ψ need not have identical truth values under every assignment or identical model sets.
Not syntactic equality. Their notation, size, normal form, and vocabulary may differ radically.
Not semantic entailment. φ |= ψ is directional and compares what all models of φ satisfy; equisatisfiability compares only whether any model exists.
Not validity equivalence. Both formulas can be satisfiable while one is valid and the other contingent.
Not model isomorphism. No one-to-one structural matching of complete models is required.
Not one-way satisfiability preservation. A sound-but-incomplete translation may preserve source witnesses yet create false target witnesses.
Not model-count preservation. Fresh-variable encodings can change how many satisfying assignments appear.
Not projection equivalence automatically. A strong encoding may guarantee that projected target models equal source models, but basic equisatisfiability asks less.
Not optimization preservation. Equal feasibility status does not preserve costs, best models, or the ordering of solutions.

Scope of Application¶

Equisatisfiability is used in SAT preprocessing, conversion to conjunctive normal form, reductions between decision problems, automated theorem proving, SMT encodings, bounded model checking, knowledge representation, and first-order transformations. It licenses replacement wherever the downstream question is only whether a model exists.

In Tseitin encoding, a fresh propositional variable names each relevant subformula and clauses constrain the name to agree with that subformula. Asserting the variable for the root produces a CNF formula of size linear in the syntax graph. Any satisfying assignment of the original extends by assigning each fresh variable its subformula’s value; any satisfying assignment of the encoding restricts to an assignment satisfying the original. The extension/restriction proof is stronger and more operationally useful than simply announcing equal SAT status.^[2]

Skolemization supplies a first-order example. Existentially quantified variables are replaced by fresh constants or Skolem functions dependent on the preceding universal variables. Under the conventional expanded-signature semantics, the Skolemized formula and source preserve satisfiability, but they are generally not equivalent formulas of one unchanged signature. Care is needed about quantifier scope, free variables, choice assumptions, and whether the transformation is being used inside a larger context.

Reductions to SAT or SMT often need more than an isolated yes/no theorem. A solver pipeline may require reconstruction of an original witness, preservation of unsatisfiable cores, proof certificates, model counts, or optimization values. Those are extra contracts layered on equisatisfiability, not consequences of it.

Clarity¶

Because satisfiability is a single Boolean property, the relation is extremely coarse. Every satisfiable formula is equisatisfiable with True; every unsatisfiable formula is equisatisfiable with False, under a shared logical setting. This does not make arbitrary replacement useful: the transformation must be effective, size-controlled, and capable of supporting whatever witness or certificate the application needs.

The carrier must be declared. On formulas interpreted over classical propositional logic, satisfiability is straightforward. In first-order, modal, finite-model, many-valued, or theory-specific settings, changing the permitted class of structures can change status. “Equisatisfiable” without the logic and semantics can therefore be incomplete.

When signatures differ, saying the formulas “have the same models” is usually ill-typed. Correct proofs use expansion and reduct: extend a source model with meanings for fresh symbols to satisfy the target, and restrict a target model to the source vocabulary to recover a source model. A direct biconditional evaluated under one common assignment is stronger than basic equisatisfiability.

Manages Complexity¶

Exact semantic preservation can be unnecessarily expensive when a procedure consumes only feasibility. Equisatisfiability deliberately discards model-by-model identity and preserves one bit: whether the model set is empty. This controlled loss enables compact encodings, solver-friendly syntax, and modular reductions.

The danger is contract mismatch. A SAT solver needs the bit and often one witness, while a model counter, optimizer, interpolant generator, or equivalence checker needs more. Treating the weaker invariant as though it preserved those outputs silently invalidates downstream conclusions. The abstraction makes the compression boundary explicit.

Abstract Reasoning¶

Logical equivalence implies equisatisfiability, but equisatisfiability does not imply logical equivalence.
Equisatisfiability is reflexive, symmetric, and transitive on a fixed carrier because it is equality after applying the Boolean Sat function.
If φ is satisfiable and φ ~sat ψ, at least one model of ψ exists, but no particular model of φ need satisfy ψ.
If ψ is an equisatisfiable encoding of φ and the solver returns UNSAT, φ is also unsatisfiable.
If the target introduces fresh variables, target assignment counts can differ even when projected source witnesses correspond.
A chain of equisatisfiable transformations remains equisatisfiable, provided every step uses compatible semantics.
One-way witness extension without reverse restriction proves only one implication of the required biconditional.
Replacing a subformula inside an arbitrary context requires a congruence property that equisatisfiability alone lacks.
If a downstream task asks whether a formula is valid, equisatisfiable replacement can change the answer.
If the logical universe is restricted to finite models, a transformation proved only for unrestricted satisfiability may fail.

Knowledge Transfer¶

The exact relation transfers among propositional SAT, first-order theorem proving, description logics, SMT, and verification whenever formulas are compared solely by model existence under declared semantics. The proof machinery changes: assignments may extend with Boolean auxiliaries, structures with Skolem functions, or theory models with introduced terms.

Outside logic, “both feasible or both infeasible” is a related kernel equivalence on constraint problems, but importing the logical name should be explicit. The cross-domain prime is Equivalence Relation; the domain accent is model-theoretic satisfiability and satisfiability-preserving transformation.

Examples¶

Tseitin CNF: auxiliary variables name subformulas, producing a linear-size CNF with the same SAT/UNSAT answer;
Skolemization: fresh functions remove existential quantifiers while preserving existence of a model under the proper signature relationship;
renaming variables: a bijective renaming is both logically equivalent up to renaming and equisatisfiable;
coarse pair: p and q ∧ r are equisatisfiable because both have models, although they disagree on many assignments;
unsatisfiable pair: p ∧ ¬p and q ∧ ¬q ∧ r are equisatisfiable because neither has a model;
non-equivalent SAT formulas: p and p ∨ q share satisfiability status but not their satisfying assignments;
failure—one-way encoding: a target admits an auxiliary assignment even when the source is unsatisfiable;
failure—substitution in context: equisatisfiable formulas replace each other beneath negation and produce different satisfiability results;
non-preserved count: one source witness extends to several auxiliary assignments, changing model count.

Structural Tensions¶

compactness vs. semantic fidelity — weaker preservation enables small encodings while discarding model identity;
decision adequacy vs. witness utility — equal status answers SAT but may not reconstruct a useful original solution;
fresh variables vs. comparability — auxiliaries prevent blow-up while making direct model-set equality unavailable;
local replacement vs. global status — the relation holds for whole formulas but is not generally substitutive inside arbitrary contexts;
broad semantics vs. proof assumptions — preservation can depend on model class, signature expansion, or quantifier conventions;
solver speed vs. auxiliary structure — more variables can yield a smaller, more propagation-friendly clause set but alter counting and proof artifacts.

Structural–Framed Character¶

Equisatisfiability is structural. Once a logic, carrier, and satisfaction relation are fixed, equality of existence status completely determines membership. Human convention chooses the formal language and use, not the relation’s internal criterion.

Structural Core vs. Domain Accent¶

The structural core is map objects to a retained invariant -> identify objects with equal invariant values. The domain accent is logical formulas mapped by Sat to model-existence status, plus the use of this coarse equivalence to justify transformations for SAT/UNSAT decision. Removing it leaves the Equivalence Relation prime.

Equivalence Relation — equisatisfiability is the kernel of the satisfiability-status function and partitions formulas into satisfiable and unsatisfiable classes.
Invariant — model-set nonemptiness is what the transformation preserves.
Translation and Conceptual Bridging — formulas change representation while one declared property survives.
Compression — model-by-model semantics are discarded to retain a decision-relevant bit.

The minimal prospective DAG placement is strict subsumption under prime:equivalence_relation.

Relationships to Other Abstractions¶

Current abstraction Equisatisfiability Domain-specific

Parents (1) — more general patterns this builds on

Equisatisfiability is a kind of Equivalence Relation Prime

equisatisfiability is the kernel of the satisfiability-status function and partitions formulas into satisfiable and unsatisfiable classes.

Hierarchy path (1) — routes to 1 parentless root

Equisatisfiability → Equivalence Relation

Neighborhood in Abstraction Space¶

Equisatisfiability sits in a sparse region of the domain-specific corpus (89^th 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¶

logical equivalence;
syntactic equivalence;
semantic entailment;
validity;
isomorphism of models;
conservative extension;
definitional equivalence;
projection or model equivalence;
parsimonious reductions preserving the number of solutions;
one-directional satisfiability preservation.

References¶

[1] Aaron R. Bradley and Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007, p. 24, https://doi.org/10.1007/978-3-540-74113-8. registry ↩

[2] University of Washington, “Equisatisfiability and Tseitin’s Transformation,” CSE 507 lecture 3, 2023, https://courses.cs.washington.edu/courses/cse507/23au/doc/L03.pdf. registry ↩a ↩b

[3] Pete Manolios, “Tseitin Transformation,” Computer-Aided Reasoning lecture 9, Northeastern University, https://www.khoury.northeastern.edu/~pete/courses/Computer-Aided-Reasoning/2021-Fall/L9.pdf. registry ↩

[4] Markus Krötzsch, Description Logic Rules, IOS Press, 2010, p. 21, https://books.google.com/books?id=Z8h7AgAAQBAJ&pg=PA21. registry

[5] “Equisatisfiability,” Wikipedia, frozen evidence packet, https://en.wikipedia.org/wiki/Equisatisfiability. registry