Skip to content
Home

Boolean satisfiability problem (SAT)

The decision problem of determining whether a propositional logic formula can be made true by some assignment of truth values; central to computational complexity and many practical solvers.

Author: Created: Updated:

Overview

The Boolean satisfiability problem, usually called SAT, asks whether there exists an assignment of truth values (true or false) to the variables of a propositional logic formula that makes the whole formula evaluate to true. If such an assignment exists the formula is called satisfiable; if no assignment makes it true the formula is unsatisfiable. SAT is a decision problem: it returns yes or no for each input formula.

Formulation and basic concepts

Formulas are commonly written in conjunctive normal form (CNF): a conjunction (logical AND) of clauses, where each clause is a disjunction (logical OR) of literals and a literal is either a variable (x) or its negation (¬x). Example CNF: (x OR ¬y OR z) AND (¬x OR y) AND (z OR w OR ¬y). A satisfying assignment picks true/false values for each variable so every clause contains at least one true literal.

Variants and special cases

  • k-SAT: Each clause has at most k literals. 3-SAT, where clauses have three literals, is a canonical NP-complete variant.
  • 2-SAT: Every clause has at most two literals. 2-SAT is solvable in polynomial time (linear time algorithms exist).
  • Horn-SAT: CNF formulas where each clause has at most one positive literal; Horn-SAT is also solvable in linear time and is important in logic programming.
  • Max-SAT: An optimization version seeking an assignment that satisfies the maximum number of clauses.

Complexity and history

SAT was the first problem proved NP-complete: the Cook–Levin theorem (circa 1971) showed that any problem in NP can be transformed to SAT in polynomial time. This established SAT as the canonical NP-complete decision problem. Shortly after, many other natural combinatorial problems were shown NP-complete, and 3-SAT became a standard hard instance used in reductions and complexity proofs.

Algorithms and practical solving

Despite its worst-case exponential complexity, modern SAT solvers handle very large instances arising in practice. Classical complete methods are based on the DPLL (Davis–Putnam–Logemann–Loveland) backtracking framework enhanced with unit propagation and pure literal elimination. Contemporary solvers use conflict-driven clause learning (CDCL), sophisticated branching heuristics, restarts, and preprocessing. There are also incomplete heuristics and local search methods that work well on many benchmarks.

Applications and notable facts

SAT is widely used to encode problems from hardware and software verification, planning, scheduling, combinatorial design, and automated reasoning. Many verification tasks are translated into SAT to leverage efficient solvers. Research areas include benchmarking, SAT competitions, and the study of random SAT instances exhibiting phase transitions between satisfiable and unsatisfiable regimes. The practical success of SAT solvers makes the problem both a theoretical cornerstone and a powerful engineering tool.

SAT belongs to propositional logic; its extension to quantified Boolean formulas (QBF) raises the complexity to higher classes in the polynomial hierarchy. Satisfiability should be distinguished from logical entailment: SAT asks for existence of a model that satisfies a formula, while entailment asks whether every model of one formula also satisfies another. Understanding these relationships is central in logic, complexity theory, and automated deduction.

Terminology

A propositional formula consists of variables, parentheses, and the propositional conjunctions conjunction ("and", often notated ∧), disjunction ("or", ∨), and negation ("not", ¬). A variable can take either the value true or the value false. A literal is an occurrence of a variable (positive literal) or its negation (negative literal). A literal is called pure if it occurs in only one occurrence, that is, either positive or negative. A monomial is a finite set of literals that are exclusively conjunctively connected. A clause is a finite set of literals that are exclusively disjunctively linked. A unit clause is a clause consisting of only a single literal. A Horn clause is a clause with at most one positive literal.

A propositional formula is in conjunctive normal form (KNF) if it consists only of conjunctions of clauses. A Horn formula is in conjunctive normal form if it consists solely of Horn clauses. The formula {\displaystyle (x_{1}\lor \lnot x_{2})\land (\lnot x_{1}\lor x_{2}\lor x_{3})\land \lnot x_{1}} is in conjunctive normal form. However, since only the first and third clauses are Horn clauses, it is not a Horn formula. The third clause is a unit clause.

A propositional formula is in disjunctive normal form (DNF) if it consists only of disjunctions of monomials. The formula {\displaystyle (x_{1}\land \lnot x_{2})\lor (\lnot x_{1}\land x_{2}\land x_{3})\lor \lnot x_{1}}is in disjunctive normal form.

Definition and variants

A formula Fis called satisfiable if and only if there exists an assignment of values true or false to each variable such that the formula is true. Formally, SAT is defined as the formal language

{\displaystyle SAT=\{F\ |\ F}is propositional formula and satisfiable \}

In practice, SAT is usually understood as the problem of finding out whether a formula Fsatisfiable. There are numerous variants and for most complexity classes there exists a variant of SAT which is complete with respect to this class.

Polynomial decidable variants of SAT

  • HORNSAT restricts SAT to Horn formulas given in disjunctive normal form. HORNSAT is P-complete
  • DNF-SAT restricts SAT to formulas given in disjunctive normal form. DNF-SAT is decidable in polynomial time, since a formula given in DNF is satisfiable exactly if none of its monomials contains two complementary literals
  • 2-SAT restricts SAT to formulas whose clauses contain at most 2 literals. 2-SAT is decidable in linear time.

3-SAT

The problem 3-SAT restricts the number of literals to 3 literals per clause. Despite this restriction, 3-SAT is NP-complete since SAT can be reduced to 3-SAT in polynomial time. The same is true for all problems k-SAT with k > 3.

P3-SAT

An instance of problem 3-SAT consisting of p variables and q clauses can also be represented by means of a graph with (p + q) many nodes. A formula is in P3-SAT if it is in 3-SAT and this graph is planar. P3-SAT is NP-complete.

MAX-SAT and MAJ-SAT

The MAX-SAT problem is to determine the maximum number of satisfiable clauses of a given formula. MAX-SAT is NP-complete and even APX-complete. It follows that no PTAS can exist for MAX-SAT if P ≠ NP.

MAJ-SAT

MAJ-SAT is the problem of deciding whether the majority of all possible variable assignments satisfy the formula. MAJ-SAT is PP-complete.

QBF (QSAT)

QBF generalizes SAT for quantified propositional formulas, that is, formulas that contain quantifiers. QBF is PSPACE-complete.

Related articles

Author

AlegsaOnline.com Boolean satisfiability problem (SAT)

URL: https://en.alegsaonline.com/art/13015

Share