1 Fundamental concepts
Satisfiability is the question of whether a logical expression can be made true under some suitable interpretation. It is one of the most basic notions in formal logic because it distinguishes formulas that describe possible situations from those that are impossible under any allowed meaning. In practice, satisfiability is used to test whether a set of constraints can coexist without contradiction.
1.1 Definition of satisfiability
A formula is satisfiable if there exists at least one model, assignment, or interpretation under which the formula evaluates as true. If no such case exists, the formula is unsatisfiable. For a collection of formulas, satisfiability means that all of them can be true together in a single model.
1.2 Models, interpretations, and assignments
The meaning of satisfiability depends on the logical system being used. In propositional logic, a truth assignment gives each variable a truth value. In first-order logic, an interpretation specifies a domain of objects together with meanings for symbols such as predicates and functions. More generally, a model provides the structure in which the formula is evaluated.
1.3 Satisfiable and unsatisfiable formulas
A satisfiable formula has at least one witness of truth, while an unsatisfiable formula has none. Simple examples in propositional logic include a variable by itself, which is satisfiable, and a contradiction such as a statement conjoined with its negation, which is unsatisfiable. Sets of formulas may also be partially constrained yet still satisfiable if a consistent assignment exists.
1.4 Validity versus satisfiability
Validity and satisfiability are related but not identical. A valid formula is true in every model, whereas a satisfiable formula is true in at least one model. Some formulas are both valid and satisfiable, while an unsatisfiable formula is never valid. Negation links the two notions: a formula is valid exactly when its negation is unsatisfiable.
2 Satisfiability in different logics
Different logical systems use different semantics, so satisfiability must be understood relative to the rules of each system. Despite these differences, the central idea remains the same: determine whether some admissible interpretation makes the formula true.
2.1 Propositional satisfiability
In propositional logic, satisfiability asks whether truth values can be assigned to variables so that a formula evaluates to true. This setting is especially important because it is simple enough to state precisely, yet rich enough to express many practical constraint problems.
2.1.1 Boolean variables and truth assignments
Propositional formulas are built from Boolean variables using connectives such as and, or, and not. A truth assignment gives each variable either true or false, and the formula is evaluated mechanically from those choices. The satisfiability question is whether at least one such assignment makes the entire formula true.
2.1.2 CNF and DNF forms
Two common normal forms are conjunctive normal form and disjunctive normal form. A formula in CNF is a conjunction of clauses, each clause being a disjunction of literals, and this format is widely used in automated solving. DNF expresses a formula as a disjunction of conjunctions and is often useful for conceptual analysis, though less common in large-scale solving.
2.2 First-order satisfiability
First-order logic extends propositional logic with quantifiers, variables ranging over objects, and symbols for relations and functions. Satisfiability in this setting asks whether there is some structure in which the quantified formula holds, which makes the problem far more expressive and generally more difficult.
2.2.1 Domains and quantifiers
A first-order formula is evaluated over a domain of objects. Quantifiers such as “for all” and “there exists” range over that domain, so satisfiability depends not only on truth values but also on the chosen universe and the interpretation of symbols. Even simple-looking formulas can have subtle satisfiability behavior because of the interaction between quantification and structure.
2.2.2 Herbrand interpretations
Herbrand interpretations are a special way of studying first-order satisfiability by focusing on terms built from the formula itself. They replace arbitrary domains with term-based structures, which can simplify certain theoretical treatments. This approach is especially useful in automated theorem proving and logic programming.
2.3 Modal satisfiability
Modal logic adds operators that talk about necessity and possibility. Satisfiability in modal logic asks whether a formula can be true at some world in a model of possible worlds, subject to accessibility relations between worlds.
2.3.1 Possible worlds semantics
In possible worlds semantics, a modal formula is evaluated relative to a world within a model. Modal operators refer to other worlds reachable from the current one, according to the model’s accessibility relation. A formula is satisfiable if there is some world in some model where it holds.
2.3.2 Frame conditions
Modal satisfiability can depend on structural constraints on the accessibility relation, called frame conditions. Properties such as reflexivity, symmetry, and transitivity lead to different modal systems and different satisfiability behaviors. These conditions shape which formulas are possible in a given modal framework.
2.4 Satisfiability in non-classical logics
Non-classical logics alter some of the assumptions of classical logic, so satisfiability must be redefined accordingly. These systems are often designed to capture additional notions such as constructibility, time, or resource sensitivity.
2.4.1 Intuitionistic logic
In intuitionistic logic, truth is tied to proof or constructive evidence rather than to classical bivalence. As a result, satisfiability is interpreted through models that reflect constructive semantics. Some formulas that are classically satisfiable behave differently in intuitionistic settings.
2.4.2 Temporal logic
Temporal logic introduces operators for time, such as “always,” “eventually,” and “until.” Satisfiability asks whether a formula can hold at some point in a temporal structure. This is useful for describing evolving systems, since the model must account for sequences of states.
3 Decision problems and complexity
Satisfiability is not only a semantic notion but also a computational problem. Once a logic is fixed, one can ask whether there is an algorithm that decides satisfiability and how much computational resources such an algorithm requires.
3.1 Satisfiability problem
The satisfiability problem, often written as SAT in the propositional case, asks whether a given formula has a model. In other logics, analogous decision problems may be defined with different names or restrictions. The central challenge is to determine existence efficiently, not merely to verify a proposed model.
3.2 NP-completeness of SAT
Propositional satisfiability is a landmark example of an NP-complete problem. This means that it lies in NP and that every problem in NP can be reduced to it in polynomial time. Its centrality comes from both its theoretical difficulty and its broad expressive power.
3.3 Complexity classes and reductions
Complexity classes organize satisfiability problems by the resources needed to solve them. Reductions are used to compare one problem with another by transforming instances while preserving satisfiability. These tools allow researchers to classify fragments of logic according to how hard their satisfiability questions are.
3.4 Decidability and undecidability
Some satisfiability problems are decidable, meaning an algorithm can always answer yes or no in finite time. Others are undecidable, so no such general algorithm exists. First-order satisfiability is a classic example of an undecidable problem in full generality, even though useful restricted fragments remain decidable.
4 Algorithms and methods
A wide range of methods has been developed to test satisfiability, from simple exhaustive procedures to highly optimized solvers. The best choice depends on the logic, the formula format, and the size of the instance.
4.1 Truth-table methods
Truth tables enumerate all possible assignments to propositional variables and check whether any one satisfies the formula. This method is straightforward and conceptually transparent. However, it becomes infeasible quickly because the number of assignments grows exponentially with the number of variables.
4.2 Resolution
Resolution is an inference rule that derives new clauses from existing ones until a contradiction is found or no further progress can be made. In propositional logic, it provides a systematic method for proving unsatisfiability. Its popularity comes from its clean proof-theoretic structure and its close connection to automated reasoning.
4.3 DPLL procedure
The DPLL procedure is a backtracking search algorithm for propositional satisfiability. It explores candidate assignments recursively while simplifying the formula along the way. Its use of pruning and deterministic simplifications made it a major step beyond naive exhaustive search.
4.4 Modern SAT solvers
Modern SAT solvers combine search, simplification, and heuristic guidance to handle very large formulas efficiently. They are among the most successful tools in symbolic computation and frequently solve instances far beyond what brute-force methods could manage. Their performance comes from a combination of clever implementation and strong algorithmic ideas.
4.4.1 Unit propagation
Unit propagation is a simplification rule that forces a variable’s value when a clause has only one remaining unassigned literal. This can trigger further forced assignments and often reduces a problem substantially before search continues. It is one of the most important practical mechanisms in SAT solving.
4.4.2 Backtracking and learning
Backtracking allows a solver to undo decisions when a chosen branch fails. Learning techniques record information from conflicts so that similar mistakes are avoided later in the search. Together, these methods greatly improve efficiency by reducing repeated work.
4.5 Model finding in first-order logic
For first-order logic, satisfiability is often approached through model finding rather than simple exhaustive enumeration. The goal is to construct a structure that interprets the formula consistently, often using search procedures, instantiation methods, or constraint-based techniques. Because the space of possible models is vast, these methods are usually specialized to restricted theories or finite domains.
5 Important variants
Satisfiability appears in several closely related problem forms, each adapted to a different logical setting or application area. These variants preserve the same basic question while changing the kinds of expressions or constraints involved.
5.1 Boolean satisfiability problem (SAT)
SAT is the classic propositional satisfiability problem. Given a Boolean formula, the task is to determine whether some assignment of truth values makes it true. It is the standard benchmark for studying satisfiability in computer science.
5.2 k-SAT
k-SAT restricts formulas to CNF expressions where each clause has at most k literals. The case k = 3 is especially important because it remains NP-complete while having a highly structured form. These restricted versions are useful for theory as well as for complexity reductions.
5.3 Constraint satisfiability
Constraint satisfiability concerns whether a set of constraints over variables can be jointly satisfied. The constraints may involve arithmetic relations, finite-domain conditions, or other structured requirements. This framework underlies many practical solving systems beyond pure Boolean logic.
5.4 Quantified Boolean formulas
Quantified Boolean formulas extend SAT by allowing universal and existential quantifiers over Boolean variables. They are a natural generalization of propositional satisfiability and are used to represent alternating choices. Their satisfiability problem is computationally harder than ordinary SAT and is important in complexity theory.
5.5 Satisfiability modulo theories
Satisfiability modulo theories, often abbreviated SMT, asks whether a logical formula is satisfiable with respect to both Boolean structure and a background theory such as arithmetic or arrays. This approach combines SAT-style search with specialized reasoning about the chosen theory. It is widely used in verification and program analysis.
6 Applications
Satisfiability is valuable wherever one must determine whether a collection of requirements can be jointly fulfilled. Its applications range from formal verification to search problems that can be encoded as logical constraints.
6.1 Hardware verification
In hardware verification, satisfiability methods check whether circuits obey specified properties. A violation can often be expressed as a formula whose satisfiability indicates the existence of an error state. This makes SAT and SMT tools effective for finding counterexamples in complex designs.
6.2 Software verification
Software verification uses satisfiability to analyze program behavior, especially for assertions, control flow, and memory conditions. Logical encoding can reveal whether a program path leads to an error or whether a property holds under all relevant inputs. These techniques are central to bug finding and formal assurance.
6.3 Planning and scheduling
Planning and scheduling problems can often be encoded as satisfiability instances. A plan exists when the encoded constraints describing actions, resources, and time steps are jointly satisfiable. This allows search over large decision spaces to be handled by general-purpose solvers.
6.4 Artificial intelligence
In artificial intelligence, satisfiability supports reasoning, inference, and search under constraints. It is used in knowledge representation, diagnosis, and combinatorial optimization. The ability to translate problem domains into logical form makes satisfiability a versatile AI tool.
6.5 Formal mathematics and proof systems
Satisfiability also plays a role in formal mathematics and proof assistants. It helps determine whether assumptions are consistent and can aid in checking proof obligations. In this context, satisfiability complements theorem proving by identifying models or exposing contradictions.
7 Related concepts
Satisfiability is connected to several fundamental logical notions that describe how formulas interact with models, derivations, and collections of statements. These relationships help clarify its place in the broader theory of logic.
7.1 Consistency of formula sets
A set of formulas is consistent if it does not entail a contradiction. In many logical systems, consistency is closely linked to satisfiability: a set is satisfiable exactly when it can all hold together in some model. This makes consistency a structural companion to satisfiability.
7.2 Entailment and consequence
Entailment concerns whether one formula or set of formulas logically implies another. If a premise set entails a conclusion, then every model of the premises is also a model of the conclusion. Satisfiability is the counterpart question of whether there exists at least one model at all.
7.3 Completeness theorems
Completeness theorems connect semantic truth with syntactic provability. They show, in suitable systems, that what is true in all models can be derived by formal proof. This linkage is essential for understanding how satisfiability interacts with proof methods.
7.4 Compactness and satisfiability
The compactness principle states that if every finite subset of a set of formulas is satisfiable, then the whole set is satisfiable, in suitable logics. This result has deep consequences for model theory and logic. It allows infinite collections of constraints to be studied through their finite parts.
8 Historical development
The study of satisfiability grew from foundational work in logic into a major area of computation. Its history reflects the gradual shift from abstract semantic questions to algorithmic methods with practical impact.
8.1 Early logical foundations
Early formal logic established the idea that statements could be analyzed in terms of models and truth conditions. The development of symbolic logic made it possible to ask whether formulas were possible or contradictory in a rigorous way. These foundations provided the semantic framework for modern satisfiability theory.
8.2 Emergence of automated reasoning
Automated reasoning developed as logicians and computer scientists sought mechanical methods for proof and model checking. Satisfiability became central because it offered a direct way to test whether logical constraints could be met. The growth of theorem proving and formal methods strengthened its importance.
8.3 SAT solving in practice
SAT solving became especially influential as increasingly powerful solvers were developed and applied to real problems. Improvements in search, conflict handling, and preprocessing allowed practical instances of great size to be handled efficiently. This turned satisfiability from a primarily theoretical concept into a core technology for verification and constraint solving.