Hubbry Logo
SatisfiabilitySatisfiabilityMain
Open search
Satisfiability
Community hub
Satisfiability
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Contribute something
Satisfiability
Satisfiability
Satisfiability
View on Wikipedia
from Wikipedia

In mathematical logic, a formula is satisfiable if it is true under some assignment of values to its variables. For example, the formula is satisfiable because it is true when and , while the formula is not satisfiable over the integers. The dual concept to satisfiability is validity; a formula is valid if every assignment of values to its variables makes the formula true. For example, is valid over the integers, but is not.

Formally, satisfiability is studied with respect to a fixed logic defining the syntax of allowed symbols, such as first-order logic, second-order logic or propositional logic. Rather than being syntactic, however, satisfiability is a semantic property because it relates to the meaning of the symbols, for example, the meaning of in a formula such as . Formally, we define an interpretation (or model) to be an assignment of values to the variables and an assignment of meaning to all other non-logical symbols, and a formula is said to be satisfiable if there is some interpretation which makes it true.[1] While this allows non-standard interpretations of symbols such as , one can restrict their meaning by providing additional axioms. The satisfiability modulo theories problem considers satisfiability of a formula with respect to a formal theory, which is a (finite or infinite) set of axioms.

Satisfiability and validity are defined for a single formula, but can be generalized to an arbitrary theory or set of formulas: a theory is satisfiable if at least one interpretation makes every formula in the theory true, and valid if every formula is true in every interpretation. For example, theories of arithmetic such as Peano arithmetic are satisfiable because they are true in the natural numbers. This concept is closely related to the consistency of a theory, and in fact is equivalent to consistency for first-order logic, a result known as Gödel's completeness theorem. The negation of satisfiability is unsatisfiability, and the negation of validity is invalidity. These four concepts are related to each other in a manner exactly analogous to Aristotle's square of opposition.

The problem of determining whether a formula in propositional logic is satisfiable is decidable, and is known as the Boolean satisfiability problem, or SAT. In general, the problem of determining whether a sentence of first-order logic is satisfiable is not decidable. In universal algebra, equational theory, and automated theorem proving, the methods of term rewriting, congruence closure and unification are used to attempt to decide satisfiability. Whether a particular theory is decidable or not depends whether the theory is variable-free and on other conditions.[2]

Reduction of validity to satisfiability

[edit]

For classical logics with negation, it is generally possible to re-express the question of the validity of a formula to one involving satisfiability, because of the relationships between the concepts expressed in the above square of opposition. In particular φ is valid if and only if ¬φ is unsatisfiable, which is to say it is false that ¬φ is satisfiable. Put another way, φ is satisfiable if and only if ¬φ is invalid.

For logics without negation, such as the positive propositional calculus, the questions of validity and satisfiability may be unrelated. In the case of the positive propositional calculus, the satisfiability problem is trivial, as every formula is satisfiable, while the validity problem is co-NP complete.

Propositional satisfiability for classical logic

[edit]
Main article: Propositional satisfiability

In the case of classical propositional logic, satisfiability is decidable for propositional formulae. In particular, satisfiability is an NP-complete problem, and is one of the most intensively studied problems in computational complexity theory.

Satisfiability in first-order logic

[edit]

For first-order logic (FOL), satisfiability is undecidable. More specifically, it is a co-RE-complete problem and therefore not semidecidable.[3] This fact has to do with the undecidability of the validity problem for FOL. The question of the status of the validity problem was posed firstly by David Hilbert, as the so-called Entscheidungsproblem. The universal validity of a formula is a semi-decidable problem by Gödel's completeness theorem. If satisfiability were also a semi-decidable problem, then the problem of the existence of counter-models would be too (a formula has counter-models iff its negation is satisfiable). So the problem of logical validity would be decidable, which contradicts the Church–Turing theorem, a result stating the negative answer for the Entscheidungsproblem.

Satisfiability in model theory

[edit]

In model theory, an atomic formula is satisfiable if there is a collection of elements of a structure that render the formula true.[4] If A is a structure, φ is a formula, and a is a collection of elements, taken from the structure, that satisfy φ, then it is commonly written that

A ⊧ φ [a]

If φ has no free variables, that is, if φ is an atomic sentence, and it is satisfied by A, then one writes

A ⊧ φ

In this case, one may also say that A is a model for φ, or that φ is true in A. If T is a collection of atomic sentences (a theory) satisfied by A, one writes

A ⊧ T

Finite satisfiability

[edit]

A problem related to satisfiability is that of finite satisfiability, which is the question of determining whether a formula admits a finite model that makes it true. For a logic that has the finite model property, the problems of satisfiability and finite satisfiability coincide, as a formula of that logic has a model if and only if it has a finite model. This question is important in the mathematical field of finite model theory.

Finite satisfiability and satisfiability need not coincide in general. For instance, consider the first-order logic formula obtained as the conjunction of the following sentences, where and are constants:


The resulting formula has the infinite model , but it can be shown that it has no finite model (starting at the fact and following the chain of atoms that must exist by the second axiom, the finiteness of a model would require the existence of a loop, which would violate the third and fourth axioms, whether it loops back on or on a different element).

The computational complexity of deciding satisfiability for an input formula in a given logic may differ from that of deciding finite satisfiability; in fact, for some logics, only one of them is decidable.

For classical first-order logic, finite satisfiability is recursively enumerable (in class RE) and undecidable by Trakhtenbrot's theorem applied to the negation of the formula.

Numerical constraints

[edit]
Further information: Satisfiability modulo theories and Constraint satisfaction problem

Numerical constraints[clarify] often appear in the field of mathematical optimization, where one usually wants to maximize (or minimize) an objective function subject to some constraints. However, leaving aside the objective function, the basic issue of simply deciding whether the constraints are satisfiable can be challenging or undecidable in some settings. The following table summarizes the main cases.

Constraints over reals over integers
Linear PTIME (see linear programming) NP-complete (see integer programming)
Polynomial decidable through e.g. Cylindrical algebraic decomposition undecidable (Hilbert's tenth problem)

Table source: Bockmayr and Weispfenning.[5]: 754 

For linear constraints, a fuller picture is provided by the following table.

Constraints over: rationals integers natural numbers
Linear equations PTIME PTIME NP-complete
Linear inequalities PTIME NP-complete NP-complete

Table source: Bockmayr and Weispfenning.[5]: 755 

See also

[edit]

Notes

[edit]

References

[edit]

Further reading

[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Satisfiability

View on Grokipedia
from Grokipedia
In , satisfiability is the property of a logical formula having at least one interpretation or model under which it evaluates to true. This concept applies across various logical systems, including propositional and . In propositional logic, the is the computational task of determining whether there exists an assignment of truth values (true or false) to the variables in a given Boolean formula such that the formula evaluates to true. This , often restricted to formulas in (CNF), serves as a foundational challenge in , where a positive answer yields a satisfying assignment, while a negative one confirms the formula's unsatisfiability. The significance of SAT stems from its central role in complexity theory, as it was the first problem proven to be NP-complete by in 1971 through the Cook-Levin theorem, establishing that any problem in NP can be reduced to SAT in polynomial time. This result, published in Cook's seminal paper "The Complexity of Theorem-Proving Procedures," demonstrated SAT's and sparked decades of research into approximation algorithms, , and exact solvers. Early algorithms, such as the Davis-Putnam procedure from 1960 and its extension Davis-Putnam-Logemann-Loveland (DPLL) in 1962, laid the groundwork for modern (CDCL) solvers that have dramatically improved practical performance since the 1990s. Beyond theory, SAT finds extensive applications in fields like hardware and software verification, where it models circuit behaviors for equivalence checking and automatic test pattern generation; , for planning and scheduling; and , optimizing layouts and routing in integrated circuits. Advances in SAT solvers, such as the and systems in the late and early , enabled their use in industrial-scale problems involving millions of variables, transforming SAT from a theoretical benchmark into a robust tool for real-world .

Fundamentals

Definition and Basic Concepts

Satisfiability is a core semantic property in , denoting that a logical can be made true under at least one interpretation. Intuitively, this means there exists an assignment of truth values to the formula's variables or a suitable structure in which the formula holds, capturing the idea of a formula being "possible" rather than necessarily false or always true. This concept underpins the analysis of logical systems' expressiveness and helps distinguish consistent theories from contradictory ones. Formally, given a logical language L\mathcal{L}, a formula ϕ\phi in L\mathcal{L} is satisfiable if there exists a model M\mathcal{M} (an interpretation of L\mathcal{L}'s symbols consisting of a domain and relations/functions thereon) such that M⊨ϕ\mathcal{M} \models \phi. This definition relies on the notion of satisfaction, where a model verifies the formula under a variable assignment. Alfred Tarski introduced this framework in his seminal 1933 work on truth in formalized languages, providing a rigorous semantic basis for evaluating formulas. Unsatisfiability, by contrast, indicates that no model exists for the , labeling it a contradiction that is false in every interpretation. Validity, on the other hand, requires the to hold in all models, implying it is satisfiable universally but distinguishing it from merely contingent satisfiability. These properties form a : unsatisfiable formulas are false in every interpretation, satisfiable ones are true in at least one interpretation, and valid ones are true in every interpretation. The notion of satisfiability originated in early 20th-century mathematical logic, with Leopold Löwenheim's 1915 demonstration that certain first-order formulas, if satisfiable, admit models of specific cardinalities, marking a foundational step in model theory. It was further contextualized by David Hilbert's program, launched around 1928, which aimed to establish the consistency of mathematical axiom systems through finitary methods—where consistency for first-order theories equates to the satisfiability of their axioms. Tarski's formalization in the 1930s solidified the term and its semantics amid these foundational efforts. Basic examples from propositional logic illustrate these ideas: the formula p∨¬pp \lor \neg p is satisfiable (in fact, valid), as it evaluates to true under any truth-value assignment to pp; whereas p∧¬pp \land \neg p is unsatisfiable, evaluating to false in every assignment. Such cases highlight satisfiability's role in semantic evaluation, primarily within propositional and logics.

Relation to Validity and Tautology

In logic, there exists a fundamental duality between satisfiability and validity: a ϕ\phi is valid (or a tautology) if and only if its negation ¬ϕ\neg \phi is unsatisfiable, and conversely, ϕ\phi is satisfiable if and only if it is not a contradiction (i.e., not unsatisfiable). This duality arises from the semantic definitions in classical logic, where validity means truth in every interpretation and satisfiability means truth in at least one interpretation. This relationship enables a practical reduction of the validity problem to the satisfiability problem: to determine if ϕ\phi is valid, one tests the satisfiability of ¬ϕ\neg \phi; if ¬ϕ\neg \phi is unsatisfiable, then ϕ\phi is valid. The proof of this reduction follows directly from the duality: if ϕ\phi is invalid, there exists an interpretation where ϕ\phi is false, which means ¬ϕ\neg \phi is true in that interpretation, rendering ¬ϕ\neg \phi satisfiable; thus, unsatisfiability of ¬ϕ\neg \phi confirms validity of ϕ\phi. In proof theory, this duality underpins refutation-based methods, where unsatisfiability of a (or set of ) implies the hood of its ; for instance, resolution proving operates by deriving the empty from the of a putative , establishing unsatisfiability and thus validity. Similarly, in Hilbert-style axiomatic systems, proofs establish validity by showing that the leads to a contradiction, leveraging the same unsatisfiability criterion. As an illustrative example, consider the ϕ=(p→q)→(¬q→¬p)\phi = (p \to q) \to (\neg q \to \neg p); to verify its validity, negate it to obtain ¬ϕ\neg \phi and check if ¬ϕ\neg \phi is satisfiable—finding it unsatisfiable confirms ϕ\phi as a tautology.

Propositional Satisfiability

In

In classical propositional logic, the language is defined over a of atomic propositions, usually denoted by symbols such as p,q,[r](/page/R),…p, q, [r](/page/R), \dots. Complex formulas are constructed recursively using the five standard connectives: (¬\neg), conjunction (∧\land), disjunction (∨\lor), implication (→\to), and biconditional (↔\leftrightarrow). For instance, if ϕ\phi and ψ\psi are formulas, then ¬ϕ\neg \phi, ϕ∧ψ\phi \land \psi, ϕ∨ψ\phi \lor \psi, ϕ→ψ\phi \to \psi, and ϕ↔ψ\phi \leftrightarrow \psi are also formulas. The semantics of classical propositional logic are based on two-valued truth assignments, which map each atomic proposition to one of the truth values true (T) or false (F). These assignments extend recursively to all formulas via the truth tables for the connectives: for example, [ϕ](/page/Phi)∧ψ[\phi](/page/Phi) \land \psi is true if both [ϕ](/page/Phi)[\phi](/page/Phi) and ψ\psi are true, and [ϕ](/page/Phi)→ψ[\phi](/page/Phi) \to \psi is false only if ϕ\phi is true and ψ\psi is false. A truth assignment serves as a model for a formula [ϕ](/page/Phi)[\phi](/page/Phi) if it evaluates ϕ\phi to true; thus, [ϕ](/page/Phi)[\phi](/page/Phi) is satisfiable if at least one such model exists. A set of formulas is satisfiable if there is a single truth assignment that models all of them simultaneously. To facilitate satisfiability analysis, any can be transformed into an equivalent normal form, such as (CNF)—a conjunction of disjunctions of literals—or (DNF)—a disjunction of conjunctions of literals. The process begins by converting the formula to (NNF), where negations appear only immediately before atomic propositions. The steps for this conversion are: (1) eliminate implications and biconditionals by replacing ϕ→ψ\phi \to \psi with ¬ϕ∨ψ\neg \phi \lor \psi and ϕ↔ψ\phi \leftrightarrow \psi with (ϕ→ψ)∧(ψ→ϕ)(\phi \to \psi) \land (\psi \to \phi); (2) push negations inward using , so ¬(ϕ∧ψ)\neg (\phi \land \psi) becomes ¬ϕ∨¬ψ\neg \phi \lor \neg \psi, ¬(ϕ∨ψ)\neg (\phi \lor \psi) becomes ¬ϕ∧¬ψ\neg \phi \land \neg \psi, and double negations ¬¬ϕ\neg \neg \phi simplify to ϕ\phi; (3) repeat until no negations precede complex subformulas. From NNF, CNF is obtained by distributing disjunctions over conjunctions (e.g., (a∨b)∧c(a \lor b) \land c to (a∧c)∨(b∧c)(a \land c) \lor (b \land c)), while DNF requires distributing conjunctions over disjunctions. A CNF formula is unsatisfiable if it contains an empty clause, which has no satisfying assignment. In general, however, determining the satisfiability of a CNF formula requires checking for a consistent truth assignment that satisfies all clauses simultaneously. A fundamental of classical propositional logic is that every consistent set of formulas—meaning no formula and its negation are both derivable—possesses a model. This follows from Lindenbaum's lemma, which asserts that any consistent set can be extended to a maximally consistent set, from which a truth assignment can be defined by assigning truth values according to the formulas in the set. In the propositional case, this extension is constructive due to the finite nature of proofs for contradictions. The foundations of propositional satisfiability in were laid in the 1920s through Emil Post's demonstration of the completeness and decidability of the propositional calculus, establishing that satisfiability could be algorithmically determined for any . Building on this in , Alonzo Church's investigations into logical systems further clarified the semantic underpinnings and decision procedures for propositional logic.

The

The , commonly denoted as SAT, asks whether there exists a truth assignment to the Boolean variables in a given such that the evaluates to true. It is typically formulated for formulas in (CNF), where the is a conjunction of and each is a disjunction of literals (variables or their negations). The decision version of SAT outputs yes if a satisfying assignment exists and no otherwise, with the search version seeking to find such an assignment if it exists. The Cook-Levin theorem, proved by in 1971, establishes that SAT is NP-complete. The proof demonstrates that any language accepted by a in time can be reduced in time to the satisfiability of circuits, which in turn reduces to CNF-SAT. This reduction involves simulating the nondeterministic computation as a formula where satisfiability corresponds to the existence of an accepting path. As the first problem proven to be NP-complete, SAT provided the foundation for identifying the complexity class and motivated the central open question of whether P equals NP. Important variants of SAT highlight thresholds of computational difficulty. The 2-SAT variant, restricted to clauses with at most two literals, is solvable in polynomial time—specifically linear time—via construction of an implication graph, where satisfiability is checked by ensuring no variable and its negation lie in the same . In contrast, 3-SAT, where each clause contains exactly three literals, is NP-complete, as shown by a from general SAT that pads clauses with auxiliary variables to achieve exactly three literals per clause. For illustration, consider the 3-CNF formula (p∨¬q)∧(¬p∨r)∧(q∨¬r).(p \vee \neg q) \wedge (\neg p \vee r) \wedge (q \vee \neg r). A satisfying assignment is p=⊤p = \top, q=⊤q = \top, r=⊤r = \top, which evaluates the first clause to true (since p=⊤p = \top), the second to true (since r=⊤r = \top), and the third to true (since q=⊤q = \top).

First-Order Satisfiability

Definitions and Semantics

First-order languages provide the syntactic foundation for expressing statements in first-order logic. A first-order language L\mathcal{L} includes a countable set of constant symbols CC, function symbols FF of various arities, predicate symbols PP of various arities (including equality == as a binary predicate), a countable set of variables VV, logical connectives ¬,∧,∨,→,↔\neg, \land, \lor, \to, \leftrightarrow, and quantifiers ∀\forall (universal) and ∃\exists (existential). Terms are built inductively from constants, variables, and function applications, while atomic formulas consist of predicate applications to terms (e.g., P(t1,…,tn)P(t_1, \dots, t_n)), and more complex formulas are formed using connectives and quantifiers binding variables. The semantics of are defined relative to that interpret the language. A M\mathcal{M} for L\mathcal{L} consists of a non-empty domain DD (the of discourse) and an interpretation function II that assigns to each constant c∈Cc \in C an element I(c)∈DI(c) \in D, to each nn-ary function f∈Ff \in F a function I(f):Dn→DI(f): D^n \to D, and to each nn-ary predicate p∈Pp \in P a relation I(p)⊆DnI(p) \subseteq D^n. A variable assignment v:V→Dv: V \to D maps free variables to domain elements. The satisfaction relation M⊨ϕ\mathcal{M} \models \phi (read as "M\mathcal{M} satisfies ϕ\phi under assignment vv") is defined inductively: for atomic formulas, it holds if the terms evaluate to elements satisfying the interpreted relation; connectives follow truth-functional rules (e.g., M⊨¬ϕ\mathcal{M} \models \neg \phi iff not M⊨ϕ\mathcal{M} \models \phi); and quantifiers satisfy M⊨∀xϕ\mathcal{M} \models \forall x \phi iff for all d∈Dd \in D, M⊨ϕ[v[x↦d]]\mathcal{M} \models \phi[v[x \mapsto d]], and dually for ∃\exists. Formulas in may be open (containing free variables) or closed (, with no free variables). Satisfiability is typically defined for : a sentence ϕ\phi is satisfiable if there exists a M\mathcal{M} such that M⊨ϕ\mathcal{M} \models \phi; otherwise, it is unsatisfiable. For open formulas, satisfiability can be considered relative to assignments, but the core notion aligns with the quantifier-free case of propositional satisfiability when all quantifiers are absent. Herbrand interpretations offer a for models, constructed over the Herbrand universe (ground terms generated from constants and functions) with interpretations restricted to ground atomic formulas, providing a basis for checking satisfiability in clausal forms. Skolemization is a transformation that eliminates existential quantifiers while preserving satisfiability. For a sentence in ∀x1…∀xn∃yψ(x1,…,xn,y)\forall x_1 \dots \forall x_n \exists y \psi(x_1, \dots, x_n, y), it introduces new function symbols (Skolem functions) f(x1,…,xn)f(x_1, \dots, x_n) to replace yy, yielding ∀x1…∀xnψ(x1,…,xn,f(x1,…,xn))\forall x_1 \dots \forall x_n \psi(x_1, \dots, x_n, f(x_1, \dots, x_n)); the resulting universal sentence is satisfiable the original is. This process extends to multiple quantifiers by handling dependencies from preceding universals. As an illustrative example, consider the sentence ∃x∀y(P(x,y)→P(y,x))\exists x \forall y (P(x,y) \to P(y,x)). This expresses that there exists an element xx such that for every yy, if PP relates xx to yy, then PP relates yy back to xx. The sentence is satisfiable; for instance, in a with a singleton domain and the empty interpretation for PP (), or where PP is the equality relation (self-loops only).

Decidability and Undecidability

The undecidability of satisfiability was established in 1936 through independent results by and , resolving Hilbert's negatively by showing that no general algorithm exists to determine whether a given sentence is satisfiable. Church's proof demonstrated that the problem is undecidable by reducing it to the unsolvability of the for , while Turing's work linked it directly to the undecidability of the for Turing machines. These results built on Turing's earlier 1936 demonstration of the halting problem's undecidability, providing foundational insights into the limits of formal systems in logic. The proof of undecidability proceeds by encoding the behavior of Turing machines into sentences such that the satisfiability of the resulting sentence corresponds precisely to whether the machine halts on a given input. Specifically, the encoding represents the machine's tape, states, and transition rules using predicates for positions, symbols, and configurations, with axioms ensuring that any model simulates a valid sequence. Since the is undecidable, no algorithm can uniformly decide the satisfiability of such sentences, extending to the general case. Despite the overall undecidability, certain restricted fragments of admit decision procedures. The Bernays-Schönfinkel-Ramsey class, characterized by a quantifier prefix of universal quantifiers followed by existential ones and the absence of function symbols, is decidable, with algorithms relying on finite or automata-based methods. Similarly, monadic , which limits predicates to unary (unary relations only), is decidable, as established by Löwenheim in through semantic arguments reducing validity to finite cases. An important implication arises from the Löwenheim-Skolem theorem, which states that if has an infinite model, it also has a countable model; thus, for satisfiability purposes, it suffices to consider countable , though this does not yield a decision procedure due to the encoding of undecidable problems.

Model-Theoretic Perspectives

Satisfiability in Structures

In , provides an interpretation for , and it satisfies if every sentence in the theory holds true under that interpretation. Formally, given LL consisting of relation symbols, function symbols, and constants, M=(M,{RiM}i∈I,{fjM}j∈J,{ckM}k∈K)\mathcal{M} = (M, \{R_i^{M}\}_{i \in I}, \{f_j^{M}\}_{j \in J}, \{c_k^{M}\}_{k \in K}) satisfies an LL-sentence ϕ\phi, denoted M⊨ϕ\mathcal{M} \models \phi, if the relations, functions, and constants in M\mathcal{M} make ϕ\phi true when evaluated in the domain MM. For TT, a subset of LL-sentences, M\mathcal{M} is a model of TT if M⊨ψ\mathcal{M} \models \psi for every ψ∈T\psi \in T. If TT is inconsistent, no satisfies TT, but partial models—structures satisfying finite subsets of TT—may exist and are key to broader constructions. The is a cornerstone result linking local and global satisfiability in structures. It states that a set Σ\Sigma of sentences is satisfiable (i.e., model) every finite of Σ\Sigma is satisfiable. This , first proved as a consequence of Gödel's completeness theorem and later attributed to Malcev in its general form, implies that inconsistencies in infinite theories arise from finite portions alone, enabling the construction of models for infinite axiom sets by iteratively extending finite models. In the context of semantics, where structures interpret quantifiers over domains, compactness ensures that satisfiability is preserved under finite approximations. Ultraproducts offer a powerful technique for constructing models that realize specific types while preserving satisfiability properties. Given a family of structures {Mi}i∈I\{\mathcal{M}_i\}_{i \in I} and a non-principal ultrafilter U\mathcal{U} on II, the ∏i∈IMi/U\prod_{i \in I} \mathcal{M}_i / \mathcal{U} is formed by taking equivalence classes of sequences under U\mathcal{U}- agreement; Łoś's theorem guarantees that the ultraproduct satisfies a first-order sentence if and only if the family does so U\mathcal{U}-almost everywhere. Saturated models, often obtained as ultrapowers ( of a structure with itself), are κ\kappa-saturated for some cardinal κ\kappa if they realize every consistent type of cardinality less than κ\kappa, providing maximal structures for studying satisfiability of partial theories or types. This construction is essential for embedding partial models into larger ones that satisfy extended sets of sentences. A illustrative example of satisfiability in ordered structures is the theory of real closed fields (RCF), axiomatized by field axioms, order axioms, and the intermediate value property for polynomials. The real numbers R\mathbb{R} form a model of RCF, satisfying all its sentences, while non-archimedean extensions like hyperreal fields—constructed via ultraproducts of R\mathbb{R} with respect to a non-principal ultrafilter on N\mathbb{N}—also satisfy RCF but introduce infinitesimals, demonstrating how ultraproducts yield non-standard models with the same properties. These models highlight structural properties like order-completeness in the reals, where satisfiability ensures the realization of polynomial roots and order relations. Satisfiability also connects to algebraic structures through varieties, equational classes closed under homomorphic images, subalgebras, and products. In the variety of , generated by equations like distributivity and complements, propositional satisfiability translates to the existence of a from the free Lindenbaum-Tarski (quotient by the ) onto the two-element Boolean {0,1}\{0,1\}, equivalent to the having a model where the evaluates to true. This algebraic perspective views satisfiability as the non-triviality of the , linking first-order properties in Boolean structures to interpretations.

Consistency and Models

In , a is satisfiable it is consistent, establishing that the existence of a model is equivalent to the absence of a contradiction within the . This fundamental equivalence follows from the completeness theorem, which ensures that every consistent has a model. For theories in countable languages, the Henkin construction provides a concrete method to realize this equivalence by systematically expanding the language with new constants to witness existential quantifiers and then building a model from a maximal consistent extension of the . The notion of maximal consistent sets plays a central role in this construction, extending Lindenbaum's lemma from propositional to . A maximal consistent set is a consistent that cannot be properly extended while remaining consistent, and such sets determine the truth values of all in the . By interpreting the domain as the set of these consistent and defining satisfaction recursively based on the logical connectives and quantifiers, a model can be obtained that satisfies exactly the sentences in the maximal consistent set. This approach yields a for any consistent . The omitting types theorem further refines the control over model construction by specifying conditions under which a model of a can avoid realizing certain types—consistent sets of formulas with a single free variable that describe possible behaviors of elements. For a complete countable in a countable , if a type over a countable set is not isolated (principal), there exists a model of the that omits that type entirely. This , proved using a variant of the Henkin construction that prioritizes omitting the specified formulas, allows for the isolation of models with desired properties while preserving satisfiability. These proof-theoretic tools extend to applications in non-classical logics, where satisfiability is characterized relative to specialized models. In , for instance, satisfiability corresponds to the existence of a Kripke model—a partially ordered frame where atomic propositions are persistent upward, and complex formulas satisfy monotonicity conditions under the intuitionistic connectives. A theory is intuitionistically satisfiable if it has such a model, linking consistency in the intuitionistic proof system to this semantic notion via a completeness theorem. A prominent example illustrates these connections: Peano arithmetic, a axiomatizing the natural numbers, is consistent and thus satisfiable, admitting models beyond the standard natural numbers. Its consistency, relative to stronger systems like Zermelo-Fraenkel , ensures the existence of non-standard models via , where the ordering type consists of the standard naturals followed by densely ordered copies of the integers. These non-standard models satisfy all theorems of Peano arithmetic but include "infinite" elements larger than any standard natural number, demonstrating how satisfiability captures broader interpretations consistent with the theory's axioms.

Computational Dimensions

Complexity Theory

The (SAT), which asks whether there exists a truth assignment to the variables of a in that makes the formula true, is the canonical NP-complete problem. This was established by in 1971 through a from the general problem of verifying computations to SAT, demonstrating that every problem in NP reduces to SAT. The 3-SAT variant, restricted to clauses with at most three literals, is also NP-complete, as shown via a straightforward sparsification reduction from general SAT. Extensions to quantified Boolean formulas (QBF), where universal and existential quantifiers alternate over propositional variables, elevate the complexity to PSPACE-completeness; this result follows from a reduction showing that evaluating such formulas captures the power of alternating s, as proven by Stockmeyer and Meyer in 1973. In , the complexity of satisfiability varies significantly across fragments. The monadic fragment, limited to unary predicates, has an NEXPTIME-complete satisfiability problem, with hardness arising from encodings of exponential-time computations and membership via automata-based decision procedures. Similarly, the two-variable fragment (FO²), allowing only two distinct variables in formulas, is NEXPTIME-complete for satisfiability, as demonstrated by Grädel, Kolaitis, and Vardi in 1997 through reductions from succinct alternating Turing machines and nondeterministic exponential-time algorithms exploiting finite model properties. Parameterized complexity provides a finer-grained of SAT, revealing fixed-parameter tractable (FPT) cases when structural parameters are bounded. For instance, SAT is FPT when parameterized by the of the primal graph (where vertices represent variables and edges connect variables in the same ), solvable in time O(2O(tw)n)O(2^{O(tw)} n) via dynamic programming on tree decompositions, as explored in parameterized surveys by Szeider (2003). play a central role in establishing these hardness results; the polynomial-time from 3-SAT to graph 3-coloring, due to Karp (1972), constructs a graph where variables correspond to bipartitioned vertices and clauses to connector gadgets ensuring colorings reflect satisfying assignments, while the to builds a graph with vertices for literals and edges enforcing coverage without contradictions. Recent advances up to 2025 have illuminated average-case complexity in random SAT instances, where the around clause-variable ratio 4.26 remains a benchmark for empirical , with new generative models showing that structured random instances can evade efficient solvers more effectively than uniform ones, as analyzed in Fichte et al.'s 2023 overview of SAT evolution. Quantum implications for SAT complexity suggest potential speedups in average-case scenarios; for example, the quantum approximate optimization (QAOA) has been shown to outperform classical heuristics on certain planted SAT instances with up to 30 variables, though worst-case persists under the model, per Boulebnane and Montanaro's 2024 empirical study in PRX Quantum.

Algorithms and Solvers

The development of algorithms for solving the (SAT) has been driven by the need for practical tools to handle large-scale instances, given the problem's computational challenges. Early systematic approaches rely on search, while modern techniques incorporate learning mechanisms and heuristics to prune the search space efficiently. These methods form the backbone of contemporary SAT solvers, enabling applications in verification, , and optimization. The Davis–Putnam–Logemann–Loveland (DPLL) algorithm, introduced in 1962, is a foundational complete backtracking procedure for deciding SAT. It operates by recursively selecting an unassigned variable, assigning it a truth value, and propagating implications through unit propagation—simplifying the formula by setting literals that must be true based on unit clauses (clauses with a single literal). Additionally, DPLL applies pure literal elimination, assigning values to literals that appear only positively or negatively across all clauses to avoid conflicts. If a contradiction arises (e.g., an empty clause), the algorithm backtracks by flipping the assignment of the most recent variable and continues the search. This systematic enumeration ensures completeness but can be inefficient for large formulas due to exponential worst-case time complexity. Building on DPLL, (CDCL) emerged in the late 1990s and early 2000s as a powerful extension, dramatically improving performance on real-world instances. CDCL enhances by analyzing conflicts—situations where unit propagation leads to an empty —and deriving new "learnt" clauses from the implication graph, which captures propagation dependencies. These learnt clauses are added to the original , generalizing the reason for the conflict and preventing similar failures in future searches. To manage memory, CDCL solvers periodically restart the search from a fresh assignment and incorporate activity-based heuristics, such as the VSIDS (Variable State Independent Decaying Sum) for variable selection, which prioritizes recently involved variables. Restarts help escape deep but unproductive branches, while non-chronological backjumping jumps back to the deepest level responsible for a conflict, rather than the immediate . In contrast to complete methods like CDCL, incomplete local search algorithms offer heuristics for approximating solutions to large, random, or structured SAT instances where exact solving is impractical. WalkSAT, proposed in 1993, is a prominent local search technique that starts with a and iteratively flips variable values to reduce unsatisfied clauses. It selects an unsatisfied clause at random and, for each literal in it, computes a "noise" probability: with high probability (e.g., 0.5), it flips a variable that breaks the fewest additional clauses (greedy move); otherwise, it flips a random variable in the clause to escape local minima. This balance of greediness and randomness enables WalkSAT to find satisfying assignments quickly for many industrial benchmarks, though it may fail on unsatisfiable instances. Prominent open-source SAT solvers implement these algorithms with optimizations for speed and scalability. MiniSat, developed in 2003, is a minimalist CDCL solver emphasizing simplicity and extensibility, featuring efficient data structures like watched literals for fast and lazy clause minimization to retain only useful learnt . It won multiple categories in early SAT competitions and influenced subsequent designs. Glucose, released in 2009, extends CDCL with a clause quality predictor based on literal block distance (LBD), which measures how "general" a learnt clause is by counting unique decision levels among its literals; low-LBD clauses are prioritized for retention during minimization, improving learning effectiveness. Glucose has dominated SAT competitions in application tracks, solving instances with millions of . Annual SAT competitions, organized since 2002, benchmark solvers on diverse real-world and crafted instances, fostering innovations like better preprocessing and parallelization; for example, winners have solved over 99% of industrial benchmarks from 2002, compared to under 50% by early DPLL-based tools. To illustrate DPLL, consider a small 3-SAT instance: ϕ=(x1∨¬x2∨x3)∧(¬x1∨x2∨¬x3)∧(x1∨x2∨x3)\phi = (x_1 \lor \neg x_2 \lor x_3) \land (\neg x_1 \lor x_2 \lor \neg x_3) \land (x_1 \lor x_2 \lor x_3). The algorithm begins by selecting x1x_1 (via some ) and assigning x1=⊤x_1 = \top. Unit propagation yields no immediate units, so it proceeds to x2=⊤x_2 = \top; now, the third is satisfied, but on the first two leads to no conflict. Assigning x3=⊤x_3 = \top satisfies all clauses, yielding a model {x1=⊤,x2=⊤,x3=⊤}\{x_1 = \top, x_2 = \top, x_3 = \top\}. If to x3=⊥x_3 = \bot caused a conflict (e.g., via pure literal), it would flip earlier choices until success or exhaustion proves unsatisfiability. This step-by-step process highlights DPLL's reliance on to prune invalid branches early.

Extensions and Applications

Finite and Restricted Domains

In , the satisfiability problem for restricts attention to interpretations over finite universes, yielding distinct decidability properties compared to the general case, where satisfiability is undecidable. A notable decidable fragment is monadic first-order logic, which employs only unary predicates. Its satisfiability over finite structures is decidable. Ehrenfeucht-Fraïssé games offer a combinatorial of elementary equivalence for finite models, directly informing satisfiability assessments. In an m-round game played on two finite structures A and B, the spoiler selects elements alternately in each structure, while the duplicator responds to maintain a partial ; the duplicator's winning strategy implies that A and B agree on all sentences of quantifier rank at most m. These games prove inexpressibility results, such as the non-first-order definability of even-length paths in finite graphs, by showing duplicator wins against structures distinguishing the property. Applications of finite-domain satisfiability extend to problems (CSPs) in , where variables range over finite sets and relations impose restrictions. Finite-domain CSPs reduce to SAT by encoding each variable-domain value pair as a , with clauses enforcing at-most-one and at-least-one selections per variable alongside ; for instance, in , clauses prohibit adjacent vertices from sharing colors. This reduction leverages optimized SAT solvers for practical solving, with sparse encodings often preferred for their linear clause growth despite larger variable counts. The Immerman-Vardi provides a foundational result on decidability in finite structures, establishing that with least fixed points (FO(LFP)) captures all properties computable in polynomial time on ordered finite models. This links the expressive power of FO(LFP) to the P, particularly for on ordered finite structures. For example, satisfiability of graph queries on finite databases—such as ∃x1 … ∃xk-1 ∧0 ≤ i < k E(xi, xi+1) for a path of length k in a —arises in query evaluation and static analysis, where finite models represent bounded data. While general finite first-order satisfiability is undecidable, as shown by reducing from the to finite models with binary relations, restricted forms like monadic queries remain tractable for database verification.

Satisfiability Modulo Theories

(SMT) extends the propositional satisfiability problem by determining whether formulas, combining structure with constraints from specific mathematical theories, admit a model that satisfies both the Boolean and theoretical aspects. These theories provide interpretations for non- symbols, such as arithmetic operations or bit-vector manipulations, enabling SMT to handle real-world constraints like linear inequalities or equality over uninterpreted functions. Unlike pure satisfiability, SMT solvers leverage decidable fragments of to ensure termination for supported theories, making it suitable for applications requiring precise reasoning over infinite domains. Prominent SMT solvers include Z3, developed by , which integrates a DPLL-style solver with theory-specific decision procedures through lazy proving, where the Boolean engine generates candidates that are checked and refined against constraints. Similarly, CVC5, an of the CVC4 solver from Stanford and the , employs a combination of eager and lazy approaches for efficient handling of mixed theories, supporting a wide range of logics including quantifiers and non-linear arithmetic. This integration allows SMT solvers to build upon established SAT techniques as the backbone while extending capabilities to theory atoms. Key theories in SMT include equalities with uninterpreted functions (EUF), which models abstract relations without predefined semantics, decidable via congruence closure algorithms that track equalities induced by function applications. Linear real arithmetic (LRA) addresses linear inequalities over real numbers, proven decidable by methods like the adapted for satisfiability, ensuring efficient resolution of systems like ax+by≤cax + by \leq c. Combinations of such theories, under conditions like stable , allow modular decision procedures, though some extensions like bit-vectors introduce fixed-width operations for hardware modeling. SMT finds extensive use in , particularly bounded , where it encodes program paths with arithmetic constraints to detect errors in safety-critical systems like operating system kernels. In hardware design, SMT verifies properties of circuits and protocols by modeling bit-vector operations and timing constraints, facilitating equivalence checking and fault detection in VLSI systems. For instance, consider the (x>5∧y=x+1)∧¬(y>5)(x > 5 \land y = x + 1) \land \lnot (y > 5) over the of real arithmetic; this is unsatisfiable because it implies x>5x > 5 and y=x+1>6y = x + 1 > 6, but ¬(y>5)\lnot (y > 5) means y≤5y \leq 5, leading to a contradiction in the linear constraints, revealed by methods like the . As of 2025, recent advances include techniques for strategy synthesis in SMT solvers, such as the SIRISMT framework, enhancing efficiency for complex theories.

References

  1. https://www.cs.utexas.edu/~dnp/frege/validity-and-satisfiability-in-predicate-logic.html
  2. https://www.cs.princeton.edu/courses/archive/fall21/cos326/lec/23-01-sat.pdf
  3. https://sat.inesc-id.pt/~ines/sac10.pdf
  4. https://dl.acm.org/doi/10.1145/800157.805047
  5. https://www.cs.toronto.edu/~sacook/homepage/1971.pdf
  6. https://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf
  7. https://people.eecs.berkeley.edu/~sseshia/219c/lectures/SATSolving.pdf
  8. https://cacm.acm.org/research/the-silent-revolution-of-sat/
  9. https://plato.stanford.edu/entries/tarski-truth/
  10. https://plato.stanford.edu/entries/hilbert-program/
  11. https://www.researchgate.net/publication/239902790_A_History_of_Satisfiability
  12. https://www.cs.cmu.edu/~15414/f18/lectures/13-dpll.pdf
  13. https://courses.cs.washington.edu/courses/cse507/19au/doc/L03.pdf
  14. https://courses.fit.cvut.cz/BI-ALO/robinson-resolution.pdf
  15. https://www.logic.at/people/leitsch/resolv.pdf
  16. https://builds.openlogicproject.org/content/propositional-logic/syntax-and-semantics/syntax-and-semantics.pdf
  17. https://www.sciencedirect.com/topics/computer-science/negation-normal-form
  18. https://arxiv.org/abs/1609.07379
  19. https://www.mat.uniroma2.it/~pasquale/dida/aa2223/asd2/aspvall1979linear.pdf
  20. https://perso.limos.fr/~palafour/PAPERS/PDF/Garey-Johnson79.pdf
  21. https://archive.org/details/grundzugedertheo0027hilb
  22. https://www.humanities.mcmaster.ca/~hitchckd/Tarski.pdf
  23. https://math.ucsd.edu/~sbuss/ResearchWeb/herbrandtheorem/paper.pdf
  24. https://www.cs.nmsu.edu/historical-projects/Projects/FoLundecidability.pdf
  25. https://arxiv.org/abs/1706.03949
  26. https://www.researchgate.net/publication/378115545_A_Syntactic_Proof_of_the_Decidability_of_First-Order_Monadic_Logic
  27. https://plato.stanford.edu/entries/modeltheory-fo/
  28. https://plato.stanford.edu/entries/model-theory/
  29. https://iep.utm.edu/compactness/
  30. https://www.math.toronto.edu/weiss/model_theory.pdf
  31. https://people.math.wisc.edu/~hkeisler/ultraproducts-web-final.pdf
  32. https://www.math.uchicago.edu/~may/VIGRE/VIGRE2010/REUPapers/Halper.pdf
  33. https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-25/issue-1/First-order-theories-as-many-sorted-algebras/10.1305/ndjfl/1093870521.pdf
  34. https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf
  35. https://journals.aps.org/prxquantum/abstract/10.1103/PRXQuantum.5.030348
  36. http://www.cs.ox.ac.uk/michael.benedikt/readingcourse/coursenotes.pdf
  37. https://shelah.logic.at/files/213042/42.pdf
  38. https://users.dimi.uniud.it/~angelo.montanari/esslli2010-lesson1.pdf
  39. https://www.cs.ubc.ca/~hoos/SLS-Internal/ch6.pdf
  40. https://people.cs.umass.edu/~immerman/pub/query.pdf
  41. https://www.cs.rice.edu/~vardi/papers/stoc82.pdf
  42. https://homepages.inf.ed.ac.uk/libkin/papers/fmt-pods09-full-talk.pdf
  43. http://www.diva-portal.org/smash/get/diva2:818862/FULLTEXT01.pdf
  44. https://dl.acm.org/doi/pdf/10.1145/1995376.1995394
  45. https://people.eecs.berkeley.edu/~sseshia/pubdir/SMT-BookChapter.pdf
  46. https://arxiv.org/pdf/1606.04786
  47. https://www-cs.stanford.edu/~preiner/publications/2022/BarbosaBBKLMMMN-TACAS22.pdf
  48. https://hanielbarbosa.com/papers/fm2024.pdf
  49. https://scholar.colorado.edu/downloads/zw12z556v
  50. https://dl.acm.org/doi/10.24963/ijcai.2025/887
Add your contribution
Related Hubs
Contribute something
User Avatar
No comments yet.