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.

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.

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.

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.

Abstract Reasoning

1. Logical equivalence implies equisatisfiability, but equisatisfiability does not imply logical equivalence. 2. Equisatisfiability is reflexive, symmetric, and transitive on a fixed carrier because it is equality after applying the Boolean Sat function. 3. If φ is satisfiable and φ ~sat ψ, at least one model of ψ exists, but no particular model of φ need satisfy ψ. 4. If ψ is an equisatisfiable encoding of φ and the solver returns UNSAT, φ is also unsatisfiable.

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.

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

• Finite-Valued Logic — 0.80
• Compactness — 0.79
• Second-order logic — 0.79
• Formal Theory — 0.79
• Monoidal t-Norm Logic — 0.79

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