Hubbry Logo
SAT solverSAT solverMain
Open search
SAT solver
Community hub
SAT solver
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
SAT solver
SAT solver
SAT solver
View on Wikipedia
from Wikipedia

In computer science and formal methods, a SAT solver is a computer program which aims to solve the Boolean satisfiability problem (SAT). On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y. In this case, the formula is satisfiable when x is true, so the solver should return "satisfiable". Since the introduction of algorithms for SAT in the 1960s, modern SAT solvers have grown into complex software artifacts involving a large number of heuristics and program optimizations to work efficiently.

By a result known as the Cook–Levin theorem, Boolean satisfiability is an NP-complete problem in general. As a result, only algorithms with exponential worst-case complexity are known. In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s, which have contributed to dramatic advances in the ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints.[1]

SAT solvers often begin by converting a formula to conjunctive normal form. They are often based on core algorithms such as the DPLL algorithm, but incorporate a number of extensions and features. Most SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution, with an output such as "unknown" in the latter case. Often, SAT solvers do not just provide an answer, but can provide further information including an example assignment (values for x, y, etc.) in case the formula is satisfiable or minimal set of unsatisfiable clauses if the formula is unsatisfiable.

Modern SAT solvers have had a significant impact on fields including software verification, program analysis, constraint solving, artificial intelligence, electronic design automation, and operations research. Powerful solvers are readily available as free and open-source software and are built into some programming languages such as exposing SAT solvers as constraints in constraint logic programming.

Overview

[edit]
Main article: Boolean satisfiability problem

A Boolean formula is any expression that can be written using Boolean (propositional) variables x, y, z, ... and the Boolean operations AND, OR, and NOT. For example,

(x AND y) OR (x AND (NOT z))

An assignment consists of choosing, for each variable, an assignment TRUE or FALSE. For any assignment v, the Boolean formula can be evaluated, and evaluates to true or false. The formula is satisfiable if there exists an assignment (called a satisfying assignment) for which the formula evaluates to true.

The Boolean satisfiability problem is the decision problem which asks, on input a Boolean formula, to determine whether the formula is satisfiable or not. This problem is NP-complete.

Core algorithms

[edit]

SAT solvers are usually developed using one of two core approaches: the Davis–Putnam–Logemann–Loveland algorithm (DPLL) and conflict-driven clause learning (CDCL).

DPLL

[edit]
Main article: DPLL algorithm

A DPLL SAT solver employs a systematic backtracking search procedure to explore the (exponentially sized) space of variable assignments looking for satisfying assignments. The basic search procedure was proposed in two seminal papers in the early 1960s (see references below) and is now commonly referred to as the DPLL algorithm.[2][3] Many modern approaches to practical SAT solving are derived from the DPLL algorithm and share the same structure. Often they only improve the efficiency of certain classes of SAT problems such as instances that appear in industrial applications or randomly generated instances.[4] Theoretically, exponential lower bounds have been proved for the DPLL family of algorithms.[citation needed]

CDCL

[edit]
Main article: Conflict-driven clause learning

Modern SAT solvers (developed in the 2000s) come in two flavors: "conflict-driven" and "look-ahead". Both approaches descend from DPLL.[4] Conflict-driven solvers, such as conflict-driven clause learning (CDCL), augment the basic DPLL search algorithm with efficient conflict analysis, clause learning, backjumping, a "two-watched-literals" form of unit propagation, adaptive branching, and random restarts. These "extras" to the basic systematic search have been empirically shown to be essential for handling the large SAT instances that arise in electronic design automation (EDA).[5] Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019.[6] Well known implementations include Chaff[7] and GRASP.[8]

Look-ahead solvers have especially strengthened reductions (going beyond unit-clause propagation) and the heuristics, and they are generally stronger than conflict-driven solvers on hard instances (while conflict-driven solvers can be much better on large instances which actually have an easy instance inside).[citation needed]

The conflict-driven MiniSAT, which was relatively successful at the 2005 SAT competition, only has about 600 lines of code. A modern Parallel SAT solver is ManySAT.[9] It can achieve super linear speed-ups on important classes of problems. An example for look-ahead solvers is march_dl, which won a prize at the 2007 SAT competition. Google's CP-SAT solver, part of OR-Tools, won gold medals at the Minizinc constraint programming competitions in editions 2018 up until 2025.

Certain types of large random satisfiable instances of SAT can be solved by survey propagation (SP).[citation needed] Particularly in hardware design and verification applications, satisfiability and other logical properties of a given propositional formula are sometimes decided based on a representation of the formula as a binary decision diagram (BDD).

Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. All of these behaviors can be seen in the SAT solving contests.[10]

Parallel approaches

[edit]

Parallel SAT solvers come in three categories: portfolio, divide-and-conquer and parallel local search algorithms. With parallel portfolios, multiple different SAT solvers run concurrently. Each of them solves a copy of the SAT instance, whereas divide-and-conquer algorithms divide the problem between the processors. Different approaches exist to parallelize local search algorithms.

The International SAT Solver Competition has a parallel track reflecting recent advances in parallel SAT solving. In 2016,[11] 2017[12] and 2018,[13] the benchmarks were run on a shared-memory system with 24 processing cores, therefore solvers intended for distributed memory or manycore processors might have fallen short.

Portfolios

[edit]

In general there is no SAT solver that performs better than all other solvers on all SAT problems. An algorithm might perform well for problem instances others struggle with, but will do worse with other instances. Furthermore, given a SAT instance, there is no reliable way to predict which algorithm will solve this instance particularly fast. These limitations motivate the parallel portfolio approach. A portfolio is a set of different algorithms or different configurations of the same algorithm. All solvers in a parallel portfolio run on different processors to solve of the same problem. If one solver terminates, the portfolio solver reports the problem to be satisfiable or unsatisfiable according to this one solver. All other solvers are terminated. Diversifying portfolios by including a variety of solvers, each performing well on a different set of problems, increases the robustness of the solver.[14]

Many solvers internally use a random number generator. Diversifying their seeds is a simple way to diversify a portfolio. Other diversification strategies involve enabling, disabling or diversifying certain heuristics in the sequential solver.[15]

One drawback of parallel portfolios is the amount of duplicate work. If clause learning is used in the sequential solvers, sharing learned clauses between parallel running solvers can reduce duplicate work and increase performance. Yet, even merely running a portfolio of the best solvers in parallel makes a competitive parallel solver. An example of such a solver is PPfolio.[16][17] It was designed to find a lower bound for the performance a parallel SAT solver should be able to deliver. Despite the large amount of duplicate work due to lack of optimizations, it performed well on a shared memory machine. HordeSat[18] is a parallel portfolio solver for large clusters of computing nodes. It uses differently configured instances of the same sequential solver at its core. Particularly for hard SAT instances HordeSat can produce linear speedups and therefore reduce runtime significantly.

In recent years, parallel portfolio SAT solvers have dominated the parallel track of the International SAT Solver Competitions. Notable examples of such solvers include Plingeling and painless-mcomsps.[19]

Divide-and-conquer

[edit]

In contrast to parallel portfolios, parallel divide-and-conquer tries to split the search space between the processing elements. Divide-and-conquer algorithms, such as the sequential DPLL, already apply the technique of splitting the search space, hence their extension towards a parallel algorithm is straight forward. However, due to techniques like unit propagation, following a division, the partial problems may differ significantly in complexity. Thus the DPLL algorithm typically does not process each part of the search space in the same amount of time, yielding a challenging load balancing problem.[14]

Tree illustrating the look-ahead phase and the resulting cubes.
Cube phase for the formula . The decision heuristic chooses which variables (circles) to assign. After the cutoff heuristic decides to stop further branching, the partial problems (rectangles) are solved independently using CDCL.

Due to non-chronological backtracking, parallelization of conflict-driven clause learning is more difficult. One way to overcome this is the Cube-and-Conquer paradigm.[20] It suggests solving in two phases. In the "cube" phase the Problem is divided into many thousands, up to millions, of sections. This is done by a look-ahead solver, that finds a set of partial configurations called "cubes". A cube can also be seen as a conjunction of a subset of variables of the original formula. In conjunction with the formula, each of the cubes forms a new formula. These formulas can be solved independently and concurrently by conflict-driven solvers. As the disjunction of these formulas is equivalent to the original formula, the problem is reported to be satisfiable, if one of the formulas is satisfiable. The look-ahead solver is favorable for small but hard problems,[21] so it is used to gradually divide the problem into multiple sub-problems. These sub-problems are easier but still large which is the ideal form for a conflict-driven solver. Furthermore, look-ahead solvers consider the entire problem whereas conflict-driven solvers make decisions based on information that is much more local. There are three heuristics involved in the cube phase. The variables in the cubes are chosen by the decision heuristic. The direction heuristic decides which variable assignment (true or false) to explore first. In satisfiable problem instances, choosing a satisfiable branch first is beneficial. The cutoff heuristic decides when to stop expanding a cube and instead forward it to a sequential conflict-driven solver. Preferably the cubes are similarly complex to solve.[20]

Treengeling is an example for a parallel solver that applies the Cube-and-Conquer paradigm. Since its introduction in 2012 it has had multiple successes at the International SAT Solver Competition. Cube-and-Conquer was used to solve the Boolean Pythagorean triples problem.[22]

Cube-and-Conquer is a modification or a generalization of the DPLL-based Divide-and-conquer approach used to compute the Van der Waerden numbers w(2;3,17) and w(2;3,18) in 2010 [23] where both the phases (splitting and solving the partial problems) were performed using DPLL.

[edit]

One strategy towards a parallel local search algorithm for SAT solving is trying multiple variable flips concurrently on different processing units.[24] Another is to apply the aforementioned portfolio approach, however clause sharing is not possible since local search solvers do not produce clauses. Alternatively, it is possible to share the configurations that are produced locally. These configurations can be used to guide the production of a new initial configuration when a local solver decides to restart its search.[25]

Randomized approaches

[edit]

Algorithms that are not part of the DPLL family include stochastic local search algorithms. One example is WalkSAT. Stochastic methods try to find a satisfying interpretation but cannot deduce that a SAT instance is unsatisfiable, as opposed to complete algorithms, such as DPLL.[4]

In contrast, randomized algorithms like the PPSZ algorithm by Paturi, Pudlak, Saks, and Zane set variables in a random order according to some heuristics, for example bounded-width resolution. If the heuristic can't find the correct setting, the variable is assigned randomly. The PPSZ algorithm has a runtime[clarify] of for 3-SAT. This was the best-known runtime for this problem until 2019, when Hansen, Kaplan, Zamir and Zwick published a modification of that algorithm with a runtime of for 3-SAT. The latter is currently the fastest known algorithm for k-SAT at all values of k. In the setting with many satisfying assignments the randomized algorithm by Schöning has a better bound.[26][27][28]

Applications

[edit]

In mathematics

[edit]

SAT solvers have been used to assist in proving mathematical theorems through computer-assisted proof. In Ramsey theory, several previously unknown Van der Waerden numbers were computed with the help of specialized SAT solvers running on FPGAs.[29][30] In 2016, Marijn Heule, Oliver Kullmann, and Victor Marek solved the Boolean Pythagorean triples problem by using a SAT solver to show that there is no way to color the integers up to 7825 in the required fashion.[31][32] Small values of the Schur numbers were also computed by Heule using SAT solvers.[33]

In software verification

[edit]

SAT solvers are used in formal verification of hardware and software. In model checking (in particular, bounded model checking), SAT solvers are used to check whether a finite-state system satisfies a specification of its intended behavior.[34][35]

SAT solvers are the core component on which satisfiability modulo theories (SMT) solvers are built, which are used for problems such as job scheduling, symbolic execution, program model checking, program verification based on hoare logic, and other applications.[36] These techniques are also closely related to constraint programming and logic programming.

In automated planning

[edit]

SAT solvers (see Satplan) are used for search plans.[37]

In other areas

[edit]

In operations research, SAT solvers have been applied to solve optimization and scheduling problems.[38]

In social choice theory, SAT solvers have been used to prove impossibility theorems.[39] Tang and Lin used SAT solvers to prove Arrow's theorem and other classic impossibility theorems. Geist and Endriss used it to find new impossibilities related to set extensions. Brandt and Geist used this approach to prove an impossibility about strategyproof tournament solutions. Other authors used this technology to prove new impossibilities about the no-show paradox, half-way monotonicity, and probabilistic voting rules. Brandl, Brandt, Peters and Stricker used it to prove the impossibility of a strategyproof, efficient and fair rule for fractional social choice.[40]

See also

[edit]

References

[edit]
[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

SAT solver

View on Grokipedia
from Grokipedia
A SAT solver is a designed to determine whether a given formula, typically expressed in (CNF), has a satisfying assignment of truth values to its variables, or to find such an assignment if it exists. It addresses the (SAT), the of checking the of propositional logic formulas, which was the first problem proven to be NP-complete. The origins of SAT solvers trace back to the early 1960s with the development of the Davis–Putnam procedure in 1960 and its refinement into the Davis–Putnam–Logemann–Loveland (DPLL) algorithm in 1962, which introduced systematic search combined with unit propagation to efficiently prune the search space. These early complete solvers laid the foundation for modern approaches, though they were limited in handling large-scale instances due to exponential worst-case complexity. The field advanced significantly in the late 1990s and early 2000s with the introduction of (CDCL), pioneered in solvers like (1997) and (2001), which incorporate non-chronological , learned clauses from conflicts, and heuristics such as VSIDS (Variable State Independent Decaying Sum) for variable selection. CDCL-based solvers now routinely handle industrial problems with millions of variables and clauses, far surpassing the capabilities of their predecessors. SAT solvers have become indispensable tools across computer science and engineering, powering applications in hardware and , where they check for bugs in complex systems; ; tasks like configuration and optimization; and even mathematical proving, such as generating massive proofs for problems like the Pythagorean triples. Annual international SAT competitions, starting in 2002, have driven rapid innovation by benchmarking dozens of solvers on diverse real-world instances, fostering improvements in preprocessing, parallelization, and proof certification techniques like DRAT proofs. Extensions of SAT solving, including maximum satisfiability (MaxSAT), quantified Boolean formulas (QBF), and (SMT), further expand their utility in fields like and .

Fundamentals

The Boolean Satisfiability Problem

The (SAT) asks whether there exists an assignment of truth values—true or false—to a of variables such that a given evaluates to true. Formally, given a ϕ\phi over variables x1,…,xnx_1, \dots, x_n, SAT determines if there is a function σ:{x1,…,xn}→{⊤,⊥}\sigma: \{x_1, \dots, x_n\} \to \{\top, \bot\} satisfying σ⊨ϕ\sigma \models \phi. In practice, SAT instances are typically expressed in conjunctive normal form (CNF), a standardized representation consisting of a conjunction of clauses, where each is a disjunction of literals and a literal is a variable xix_i or its ¬xi\neg x_i. Thus, a CNF formula takes the form ϕ=⋀j=1mCj,\phi = \bigwedge_{j=1}^m C_j, where each Cj=⋁k=1ljljkC_j = \bigvee_{k=1}^{l_j} l_{jk} and ljk∈{xi,¬xi∣1≤i≤n}l_{jk} \in \{x_i, \neg x_i \mid 1 \leq i \leq n\}. The problem then reduces to finding an assignment that makes every true, which occurs if at least one literal in each is true under that assignment. SAT is , as proven by Stephen Cook in 1971 through a polynomial-time reduction from the acceptance problem of nondeterministic Turing machines running in polynomial time to SAT. The proof constructs a CNF formula of polynomial size that encodes all possible computation paths of the machine on a given input ww; the formula is satisfiable if and only if at least one path accepts ww, thereby simulating nondeterministic verification within NP. This establishes both membership in NP (via nondeterministic guessing and verification) and NP-hardness. A simple satisfiable CNF example is ϕ=(x1∨¬x2)∧(x2∨x3)∧(¬x1∨¬x3)\phi = (x_1 \vee \neg x_2) \wedge (x_2 \vee x_3) \wedge (\neg x_1 \vee \neg x_3), which holds true under the assignment x1=⊤x_1 = \top, x2=⊤x_2 = \top, x3=⊥x_3 = \bot. In contrast, the formula ψ=(x1)∧(¬x1)\psi = (x_1) \wedge (\neg x_1) is unsatisfiable, as no assignment can make both clauses true simultaneously. Variants of SAT include kk-SAT, which restricts clauses to exactly (or at most) kk literals. For k≥3k \geq 3, kk-SAT is NP-complete, following from a of general SAT to kk-SAT by splitting larger clauses using auxiliary variables—for instance, transforming (l1∨l2∨l3∨l4)(l_1 \vee l_2 \vee l_3 \vee l_4) into (l1∨l2∨y)∧(¬y∨l3∨l4)(l_1 \vee l_2 \vee y) \wedge (\neg y \vee l_3 \vee l_4) where yy is a new variable. For k=2k=2, 2-SAT is solvable in linear time via implication graphs, but the problem remains NP-complete for k≥3k \geq 3.

Role and Importance of SAT Solvers

SAT solvers play a pivotal role in as tools for addressing the (SAT), recognized as the canonical NP-complete problem through the Cook-Levin theorem. This status implies that SAT serves as a benchmark for the P versus NP question: a polynomial-time algorithm for SAT would resolve the millennium prize problem by showing P = NP, while the intractability of SAT in the worst case underscores the fundamental limits of efficient computation. In practice, SAT solvers enable the automated resolution of diverse real-world problems by encoding them as propositional formulas in (CNF), transforming complex decision tasks into verifiable instances. For instance, scheduling conflicts or constraints can be modeled as SAT problems, allowing solvers to determine feasible configurations without exhaustive . This encoding approach bridges theoretical logic with tangible challenges, making SAT solvers indispensable for optimization in domains where manual analysis is infeasible. Modern SAT solvers achieve remarkable efficiency gains, routinely handling industrial-scale instances with millions of variables and clauses—far surpassing brute-force methods that would require exponential time even for modest problem sizes. Their success stems from empirical optimizations that exploit problem structure, enabling solutions to instances intractable a decade ago. The interdisciplinary reach of SAT solvers extends beyond computer science, serving as a foundational engine in for planning and probabilistic reasoning, hardware and to ensure system correctness, and broader optimization tasks that inform decision-making across engineering fields. This versatility positions them as a between theoretical foundations and applied sciences. In chip design and , their deployment has yielded substantial economic impact by streamlining verification processes, reducing development timelines, and minimizing error-related costs in high-stakes industries.

Historical Development

Early Algorithms and Milestones

The Davis–Putnam algorithm, introduced by Martin Davis and in 1960, represented the first systematic computational procedure for deciding the of propositional formulas, particularly those in (CNF). The method relies on resolution to eliminate atomic formulas, combined with unit to simplify clauses containing a single literal and pure literal elimination to remove variables that appear only positively or negatively. Originally designed for quantification theory in , it reduces such problems to propositional by eliminating quantifiers through Herbrand interpretations. This approach provided a complete decision procedure, though its reliance on exhaustive resolution steps made it computationally intensive even for modest formula sizes. Building on this foundation, the emerged in 1962, developed by Davis, George Logemann, and Donald Loveland as a practical implementation for theorem proving. The key innovation was the incorporation of chronological , which replaced the full resolution phase with recursive variable assignment and propagation, allowing the algorithm to explore partial assignments and retract choices upon conflicts. This mechanism, paired with unit propagation, enabled more efficient handling of propositional instances derived from problems, marking the birth of search-based SAT solving. Early implementations demonstrated its viability for small-scale automated deduction, though hardware constraints limited its scope. In the 1970s, SAT techniques gained traction in , with systems integrating DPLL-like procedures to verify mathematical statements and logical inferences, often reducing first-order problems to propositional cases. By the 1980s, resolution-based provers such as , initiated at , advanced these methods by incorporating paramodulation and hyperresolution for equality handling, applying them successfully to complex deduction tasks in . These developments highlighted the potential of SAT solving beyond pure logic, paving the way for applications in hardware verification in the following decade where propositional encodings of circuit behaviors were analyzed. Despite these advances, early algorithms faced significant limitations, including exponential worst-case due to the branching in and the potential for exhaustive search trees. Performance on large instances was poor, as memory demands for storing clauses and assignments quickly exceeded available resources, and average-case analyses revealed behavior only for specific random distributions with low clause-variable ratios. This restricted practical applications to formulas with fewer than 100 variables until hardware improvements in the late .

Evolution to Modern Solvers

The transition from early systematic search algorithms, such as the Davis-Putnam procedure of the 1960s, to more advanced paradigms in the marked a pivotal shift in SAT solving, driven by the need to handle increasingly large industrial instances. In the mid-, the introduction of emerged as a key innovation, with the solver pioneering conflict analysis to learn from search failures and avoid redundant . This approach laid the groundwork for more efficient complete solvers by dynamically adding clauses that constrain the search space based on detected inconsistencies. A major breakthrough came in 2001 with the solver, which refined conflict-driven learning through optimized constraint propagation and introduced the Variable State Independent Decaying Sum (VSIDS) for variable selection. VSIDS assigns scores to variables based on their occurrence in recent learned , decaying older scores over time to prioritize variables involved in current conflicts, thereby guiding the search toward promising branches with minimal overhead. demonstrated 1-2 orders of magnitude speedup over predecessors like on benchmarks, establishing conflict-driven techniques as the dominant paradigm for complete SAT solving. Subsequent solvers integrated further improvements, such as dynamic and variable selection strategies, enhancing adaptability to diverse problem structures. Solvers like MiniSat (2005), known for its simplicity and efficiency, further popularized efficient CDCL implementations and dominated early SAT competitions. The establishment of annual SAT competitions beginning in 2002 further accelerated solver evolution by providing standardized benchmarks and fostering competitive optimization. Organized initially by Edward A. Hirsch, Daniel Le Berre, and Laurent Simon in conjunction with the SAT 2002 symposium, these events evaluated solvers on crafted, random, and industrial instances, revealing performance gaps and incentivizing innovations in heuristics and implementation. Competitions drove widespread adoption of techniques like VSIDS and clause learning, with winners often setting new standards that influenced subsequent developments. For instances prone to timeouts in complete solvers, the 1990s saw the rise of incomplete methods based on search, which proved effective on hard, satisfiable problems by iteratively flipping variable assignments to reduce unsatisfied clauses. Pioneering algorithms like (1992), which greedily minimizes clause violations through flips, and WalkSAT (1997), which incorporates noise for escaping optima, outperformed systematic approaches on random 3-SAT instances by factors of up to 10 in . These methods complemented complete solvers, particularly for tasks where approximate solutions sufficed. By the 2010s, the proliferation of multi-core processors prompted adaptations in SAT solving toward parallelism, enabling solvers to exploit concurrent processing for broader search coverage. Portfolio approaches, which run multiple solver configurations in parallel, and clause-sharing mechanisms, which exchange learned clauses across threads, became prominent, yielding speedups of 4-8 times on multi-core systems for industrial benchmarks. This hardware-driven evolution extended the scalability of SAT solvers to instances with millions of clauses, integrating seamlessly with established techniques like conflict-driven learning.

Core Algorithms

Davis–Putnam–Logemann–Loveland (DPLL) Algorithm

The Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a foundational complete method for deciding the of propositional formulas in (CNF), serving as the basis for most modern SAT solvers. Introduced as an improvement over earlier resolution-based techniques, it combines systematic search with rules to prune the search space efficiently. The algorithm explores partial variable assignments recursively, simplifying the formula at each step until it determines or proves unsatisfiability.

Core Components

The DPLL algorithm relies on three key inference mechanisms to reduce the formula without branching: unit propagation, pure literal elimination, and backtracking. Unit propagation identifies and satisfies unit clauses—clauses containing a single unassigned literal—by assigning the value that makes the literal true, then propagating this assignment to simplify all affected clauses by removing the literal and its occurrences. This process repeats until no unit clauses remain or an empty clause (indicating inconsistency) is detected. Unit propagation ensures that all logical consequences of an assignment are immediately applied, avoiding redundant exploration. Pure literal elimination detects literals that appear only in one polarity (all positive or all negative) across the entire formula and assigns them the value that satisfies those clauses, removing the literal and all clauses containing it. This heuristic safely reduces the number of variables without risking inconsistency, as the opposite assignment would falsify at least one clause unnecessarily. Backtracking (specifically, chronological backtracking) undoes assignments when a branch leads to inconsistency, returning to the most recent decision point and trying the alternative value. This systematic exploration builds a of variable assignments, ensuring completeness by eventually trying all possibilities if needed.

Recursive Search Procedure

The DPLL procedure operates recursively on a CNF φ and a partial assignment M (initially empty). It first applies unit propagation and pure literal elimination to simplify φ under M. If simplification yields an empty , the assignment is satisfying; if it produces an empty , the branch is unsatisfying, triggering backtrack. Otherwise, it selects an unassigned variable for branching: it recurses by setting the variable to true (simplifying φ accordingly) and, if that fails, tries false. This branching on variables, combined with simplification, drives the search toward a model or proof of unsatisfiability. Heuristics, such as choosing the variable in the shortest (shortest-first branching), guide selection to minimize the tree size in practice.

Pseudocode Outline

The following pseudocode outlines the core DPLL satisfiability check, using standard notation where φ is the CNF formula, M is the partial assignment, BCP denotes Boolean constraint propagation (combining unit propagation and pure literal elimination), and SelectVar chooses an unassigned variable:

function SAT(φ, M): if φ is empty: // No clauses left return true, M // Satisfying assignment found if φ contains empty [clause](/page/Clause): return false, nil // Unsatisfiable under M φ', M' ← BCP(φ, M) // Apply propagation and simplification if φ' contains empty [clause](/page/Clause): return false, nil if φ' is empty: return true, M' v ← SelectVar(φ') // Choose unassigned variable // Try v = true φ_true, M_true ← Simplify(φ', v=true, M') result_true, model_true ← SAT(φ_true, M_true) if result_true: return true, model_true // Backtrack and try v = false φ_false, M_false ← Simplify(φ', v=false, M') result_false, model_false ← SAT(φ_false, M_false) if result_false: return true, model_false return false, nil // Both branches fail

function SAT(φ, M): if φ is empty: // No clauses left return true, M // Satisfying assignment found if φ contains empty [clause](/page/Clause): return false, nil // Unsatisfiable under M φ', M' ← BCP(φ, M) // Apply propagation and simplification if φ' contains empty [clause](/page/Clause): return false, nil if φ' is empty: return true, M' v ← SelectVar(φ') // Choose unassigned variable // Try v = true φ_true, M_true ← Simplify(φ', v=true, M') result_true, model_true ← SAT(φ_true, M_true) if result_true: return true, model_true // Backtrack and try v = false φ_false, M_false ← Simplify(φ', v=false, M') result_false, model_false ← SAT(φ_false, M_false) if result_false: return true, model_false return false, nil // Both branches fail

This recursive structure ensures termination, as each call reduces the problem size or explores a finite branch.

Time Complexity

In the worst case, DPLL explores the full 2^n possible assignments for n variables, yielding O(2^n) time complexity, since each propagation step can take polynomial time but the branching dominates. However, unit propagation and pure literal elimination, along with branching heuristics, dramatically reduce the effective runtime on many practical instances, making it viable for formulas with hundreds of variables.

Example Walkthrough

Consider the 3-SAT instance φ = (p ∨ q) ∧ (¬p ∨ q) ∧ (¬r ∨ ¬q) ∧ (r ∨ ¬q), with variables p, q, r. Start with empty assignment M = {}.
  1. BCP: No unit clauses or pure literals initially. Select p (e.g., via heuristic). Branch p = true: Simplify to φ' = (q) ∧ (¬r ∨ ¬q) ∧ (r ∨ ¬q), M = {p=true}.
  2. BCP on φ': Unit clause (q) propagates q = true, yielding φ'' = (¬r) ∧ (r), M = {p=true, q=true}.
  3. Further BCP: Unit (¬r) propagates r = false, satisfying (¬r) but falsifying (r) to empty clause, detecting conflict → unsatisfiable branch, backtrack.
  4. Try p = false: Simplify to φ' = (q) ∧ (¬r ∨ ¬q) ∧ (r ∨ ¬q), M = {p=false}.
  5. BCP: q = true from unit (q), yielding φ'' = (¬r) ∧ (r), M = {p=false, q=true}.
  6. Further BCP: r = false from (¬r) falsifies (r), conflict → backtrack to root.
  7. Both branches on p fail, returning unsatisfiability for the root. (Note: This instance is unsatisfiable, as the first two clauses imply q = true, and the last two imply r ↔ ¬q, leading to r = false and true.)

Conflict-Driven Clause Learning (CDCL)

(CDCL) represents a pivotal advancement in SAT solving, extending the Davis–Putnam–Logemann–Loveland () algorithm by incorporating mechanisms to analyze conflicts and derive new clauses that prune the search space more effectively. The core innovation lies in conflict analysis, where an unsatisfied clause during unit propagation triggers the construction of an implication graph to trace the reasons for the conflict, ultimately generating a learned clause that explains the failure and prevents similar conflicts in future searches. This process enables non-chronological , jumping to earlier decision levels rather than strictly chronological ones, thereby accelerating convergence to satisfying assignments or proofs of unsatisfiability. The implication graph is a directed acyclic graph where vertices represent literals (both positive and negative assignments of variables), and edges denote implications derived from unit propagation or decisions. When a conflict arises—typically both a literal and its negation being implied—a special conflict vertex connects the opposing literals. Conflict analysis then resolves antecedents backward through the graph using clause resolution to derive a new clause that asserts the negation of the conflict's cause at the highest possible decision level. A key component is the First Unique Implication Point (1UIP) learning scheme, which identifies the first vertex in the graph that lies on all paths from the current decision to the conflict, ensuring the learned clause is as general as possible while remaining asserting (unit under the current partial assignment). This scheme balances clause size and explanatory power, often yielding clauses with a single literal from the current decision level for immediate propagation upon backtrack. To illustrate conflict resolution with 1UIP learning, consider a simplified outline of the process during a conflict:

function AnalyzeConflict(conflict_literal): reason = GetReason(conflict_literal) // Antecedent [clause](/page/Clause) causing conflict learned_clause = {¬conflict_literal} current_level = DecisionLevel() while True: resolve learned_clause with reason // Resolution step: remove pivots if learned_clause has only one literal from current_level: break // Reached 1UIP Update reason to antecedent of next pivot Add learned_clause to [clause](/page/Clause) database Backtrack to decision level of the asserting literal in learned_clause

function AnalyzeConflict(conflict_literal): reason = GetReason(conflict_literal) // Antecedent [clause](/page/Clause) causing conflict learned_clause = {¬conflict_literal} current_level = DecisionLevel() while True: resolve learned_clause with reason // Resolution step: remove pivots if learned_clause has only one literal from current_level: break // Reached 1UIP Update reason to antecedent of next pivot Add learned_clause to [clause](/page/Clause) database Backtrack to decision level of the asserting literal in learned_clause

This procedure traces back from the conflict, iteratively resolving until the 1UIP criterion is met, producing a clause that prunes irrelevant branches. CDCL solvers integrate advanced heuristics to enhance efficiency, notably the Variable State Independent Decaying Sum (VSIDS) for variable branching. In VSIDS, each variable maintains scores for its polarities based on their occurrence in learned clauses, incremented upon learning and periodically decayed by a factor (e.g., 1/1000th) to emphasize recent conflicts. The unassigned variable with the highest score is selected for branching, with polarity chosen to satisfy the most recent unsatisfied clause containing it. This dynamic heuristic adapts to the problem's structure, focusing the search on contentious variables. Restart strategies further bolster CDCL by periodically resetting the search trail to escape suboptimal paths, particularly in problems exhibiting heavy-tailed runtime distributions. Solvers like those employing randomized restarts increase the cutoff time geometrically (e.g., starting from 100 conflicts and doubling), preserving learned clauses across restarts to retain knowledge while exploring fresh decision sequences. This approach mitigates the risk of prolonged searches in unproductive subspaces, with empirical evidence showing speedups by orders of magnitude on structured benchmarks. The performance impact of CDCL is exemplified by the MiniSat solver, which implements these components—including 1UIP learning, VSIDS, and adaptive restarts—achieving superior results on the SAT 2003 competition benchmarks by solving 158 out of 177 industrial instances within 10,000 seconds, outperforming contemporaries like zChaff (147 solved) and BerkMin (157 solved). Such advancements underscore CDCL's role in transforming SAT solving from a theoretical into a practical tool for large-scale verification and optimization.

Advanced Techniques

Parallel and Distributed Solving

Parallel and distributed SAT solving techniques extend sequential (CDCL) methods to leverage multi-core processors and clusters, enabling significant speedups on large-scale instances by distributing computational workload. These approaches address the inherent limitations of single-threaded solvers, such as prolonged search times on hard combinatorial problems, by exploiting parallelism in the search space without altering the underlying completeness guarantees. One prominent strategy is the portfolio approach, where multiple instances of SAT solvers—often configured with diverse heuristics, parameters, or random seeds—run concurrently on the same , with the first to find a solution (or prove unsatisfiability) terminating the process. Introduced in seminal works like ManySAT, this method capitalizes on the variability in solver performance across instances, achieving speedups through complementary search behaviors rather than deep integration. Portfolio solvers typically exchange only unit or binary clauses to minimize overhead, making them suitable for shared-memory multi-core environments. In contrast, divide-and-conquer techniques partition the into independent subproblems, solving them in parallel to conquer the overall instance. The -and-conquer paradigm exemplifies this by using a lookahead solver in an initial "cube" phase to decompose the into thousands or millions of smaller —partial assignments that simplify the problem—followed by a "conquer" phase where CDCL solvers tackle each independently under assumptions. This hybrid method, which integrates traditional lookahead with modern CDCL, has demonstrated up to 20-fold speedups on challenging benchmarks like van der Waerden problems by enabling trivial across subproblems. Distributed implementations, such as Paracooba, extend this to cluster settings by assigning to remote nodes, supporting incremental solving to reuse learned information. Distributed solving often incorporates clause sharing to enhance cooperation among processes, where learned clauses from one solver are broadcast to others via , accelerating global progress. In systems like Mallob, this periodic exchange—occurring every few seconds—yields 10- to 100-fold speedups over sequential solvers on broad benchmarks by propagating conflict-driven insights without problem partitioning. To ensure verifiability, especially for unsatisfiability results, distributed clause-sharing solvers generate proofs using extensions like LRAT (a superset of DRAT), which track clause dependencies and allow reconstruction of a single, compact refutation from partial proofs across nodes. Key challenges in these paradigms include load balancing, where uneven subproblem difficulties can lead to idle processors or starvation in divide-and-conquer setups, and communication overhead, which escalates in distributed environments due to network latency during clause exchanges. Multi-core systems mitigate some overhead through shared memory but face synchronization costs, while clusters demand optimized strategies like dynamic clause filtering to balance benefits against bandwidth limits. Frameworks such as PaInleSS address these by modularly combining portfolio and divide-and-conquer with configurable sharing, supporting solvers like MiniSat variants on many-core architectures. Representative examples include PMSat, an early MPI-based parallelization of MiniSat that distributes search trees across nodes for basic portfolio-style solving, and more advanced variants like those in PaInleSS, which integrate diverse engines such as Glucose and Lingeling for competitive performance on hard instances. These developments underscore the shift toward scalable, verifiable parallel SAT solving in the 2010s and 2020s. Recent advancements as of 2025 include GPU-CPU hybrid systems like TurboSAT, which achieves up to 200x speedups on satisfiable benchmarks from the 2024 SAT Competition through gradient-guided exploration, and MallobSat winning the parallel track in the 2025 SAT Competition.

Randomized and Local Search Methods

Randomized and local search methods represent an incomplete class of approaches to solving the (SAT), prioritizing speed over guaranteed completeness by employing stochastic techniques to explore the search space. These methods begin with a of truth values to variables and iteratively modify the assignment through variable flips, aiming to minimize the number of unsatisfied clauses. Unlike systematic algorithms such as DPLL, local search avoids exhaustive and instead relies on heuristics to guide flips toward promising directions, often incorporating to escape local optima where no further improving moves are available. The WalkSAT algorithm, introduced as an enhancement to earlier greedy local search procedures, exemplifies these principles through a combination of greedy hill-climbing and probabilistic random walks. In WalkSAT, at each step, a unsatisfied is selected at random, and a variable from that clause is chosen for flipping: with probability pp (the noise parameter), a random variable is flipped to introduce exploration; otherwise, the variable whose flip breaks the fewest additional clauses is selected to maintain greediness. This randomized mechanism allows WalkSAT to navigate rugged landscapes effectively, performing well on large random 3-SAT instances where pure greedy methods stall. The algorithm was first detailed in work by Selman, Kautz, and Cohen, building on the framework to incorporate noise for better performance on hard combinatorial problems. To approximate completeness in practice, randomized local search methods often employ restarts, where the algorithm is run multiple times from fresh random assignments for short durations, pooling results across iterations to increase the likelihood of finding a satisfying assignment if one exists. This strategy leverages the independence of restarts to mitigate the risk of prolonged trapping in local minima during a single run, with cutoff lengths tuned empirically—such as geometric distributions—to balance exploration and efficiency. Seminal analysis shows that such restarts can achieve expected runtime for certain random SAT distributions under appropriate policies. Hybrid methods integrate local search with complete algorithms like DPLL to leverage their complementary strengths, particularly for time-bound applications where quick heuristics can inform systematic search. For instance, local search may preprocess instances to identify likely satisfying partial assignments or clauses to prioritize, passing refined subproblems to a DPLL solver upon timeout, thereby accelerating solution discovery on satisfiable benchmarks while retaining proof capabilities for unsatisfiability. Early demonstrations of this integration in domains highlighted dramatic speedups, solving previously intractable problems by encoding them as SAT and alternating stochastic and systematic phases. These methods excel on random and certain structured satisfiable instances, often outperforming complete solvers by orders of magnitude due to their ability to quickly locate solutions in vast spaces without overhead. However, they struggle with proving unsatisfiability, as failure to find a solution after extensive restarts provides no formal certificate, limiting their utility in verification tasks requiring rigorous disproofs. Empirical evaluations confirm their superiority on uniform random 3-SAT near the but reveal vulnerabilities to tightly coupled structured formulas where local moves yield minimal progress. Recent work as of 2025, such as DiverSAT, introduces novel heuristics to handle diverse SAT problems, enhancing performance on structured instances through diversification strategies.

Applications

Hardware and Software Verification

SAT solvers play a crucial role in hardware and by encoding system behaviors and properties as propositional satisfiability problems, enabling the detection of design errors through exhaustive search within bounded scopes. In hardware verification, SAT solvers facilitate bounded (BMC), where temporal properties are translated into SAT instances by unrolling the system's transition relation over a finite number of steps. This approach, introduced by Clarke et al. in 1999, constructs a formula [[M]]k=I(s0)∧⋀i=0k−1T(si,si+1)[[M]]_k = I(s_0) \land \bigwedge_{i=0}^{k-1} T(s_i, s_{i+1}) representing the unrolled model MM up to bound kk, conjoined with the negation of a property to check for reachable violations. If the resulting CNF formula is satisfiable, a path is extracted; otherwise, the property holds within the bound. This method has proven effective for verifying properties in complex circuits, such as microprocessors, by iteratively increasing kk until completeness is approached or proven. For circuit equivalence verification, SAT solvers reduce the problem of comparing two gate-level designs to checking the unsatisfiability of a miter circuit, which XORs corresponding outputs and feeds shared inputs into both implementations. If the miter's output cannot be asserted to 1 under any input assignment, the circuits are equivalent. This technique, leveraging CNF encodings of the gate-level netlists, has been enhanced with incremental SAT solving to handle don't-care conditions and structural optimizations, improving scalability for large designs. In practice, SAT-based equivalence checking outperforms traditional BDD methods on circuits with high or irregular structures, as demonstrated in industrial flows where it verifies retimed or optimized implementations against golden references. In , SAT solvers enable path exploration by unwinding program loops and control flows into bounded SAT instances, checking for assertion violations or undefined behaviors. The CBMC tool, developed by Kroening et al. starting in the early , applies this to ANSI-C programs by converting the unwound code into bit-precise formulas solved via integrated SAT solvers like MiniSat. CBMC has been used to verify and concurrency properties in , generating counterexamples as feasible execution traces when bugs are found. A notable involves Intel's application of SAT solvers in processor verification since the late 1990s, where they detected subtle errors in the instruction decoder, including mismatches in handling that could lead to incorrect execution. These efforts, building on post-FDIV bug lessons, integrated SAT into equivalence and property checking flows, uncovering bugs in and logic that simulation missed. To support iterative verification in evolving designs, incremental SAT solving reuses learned clauses and variable assignments across successive SAT instances, reducing redundancy in BMC unrollings or equivalence checks. Techniques like those in Eén and Sörensson (2011) maintain solver state during bound increments, enabling efficient proof of properties over increasing horizons in hardware models. This extension has been pivotal in industrial settings, where design revisions require repeated verifications without restarting from scratch, as seen in processor pipelines where incremental proofs confirm equivalence after minor gate-level changes.

Artificial Intelligence and Planning

SAT solvers play a pivotal role in , particularly in automated and knowledge representation, where complex decision-making problems are encoded as propositional instances. In classical , problems defined in languages like the (PDDL) are translated into (CNF) formulas, allowing SAT solvers to search for sequences of actions that achieve desired goals from initial states. This approach, pioneered in the early , transforms the planning task into checking the of a formula that encodes state transitions, action preconditions, and goal conditions over a fixed horizon of time steps. The GraphPlan algorithm, introduced in the mid-1990s, further advanced this paradigm by using planning graphs to generate compact CNF encodings that prune irrelevant actions and states, significantly improving efficiency over naive translations. By iteratively building layered graphs representing possible propositions and actions, GraphPlan extracts mutex relations (mutually exclusive elements) that translate directly into conflict clauses in the SAT formula, enabling faster solving for STRIPS-style domains common in PDDL. This integration of graph-based analysis with SAT solving demonstrated superior performance on benchmarks like and problems, establishing a foundation for modern planners. In conformant planning, which addresses in initial states or nondeterministic action effects without intermediate observations, SAT encodings model states as sets of possible worlds or disjunctive formulas. states are represented using literals that capture known true, known false, or unknown propositions, with actions encoded to propagate these over time steps while ensuring satisfaction across all possible trajectories. This approach compiles the problem into a SAT instance by enumerating bounded initial possibilities or using approximations for scalability, as shown in early mappings that handle through exhaustive but optimized clause generation. For instance, techniques like those compiling conformant problems to SAT via bounded initial state sets have solved instances with up to moderate levels efficiently. SAT solvers also facilitate scheduling tasks in AI, such as , by encoding constraints like availability, compatibility, and sequencing as clauses. In crew rostering, for example, variables represent assignments of duties to personnel, with clauses enforcing rules on rest periods, skill requirements, and coverage; satisfiability yields a valid roster minimizing violations or costs. This has been applied to transportation scheduling, where SAT encodings handle complex preferences and regulations, outperforming traditional on certain real-world instances by leveraging conflict-driven learning for rapid constraint propagation. Tools like the planner from the late 1990s exemplify the practical integration of SAT solvers in AI planning, combining GraphPlan's graph extraction with advanced SAT engines like WalkSAT for local search and complete solvers for optimality. automates the translation of PDDL-like inputs to CNF, incorporating mutex propagation and parallel plan extraction, and achieved competitive results in early International Planning Competitions by balancing guidance with solving. In AI theorem proving, extensions of SAT to (SMT) enable encoding fragments of by grounding quantifiers and integrating theory-specific solvers for domains like arithmetic or equality. This allows automated provers to reduce higher-level reasoning to propositional checks augmented with domain axioms, supporting tasks like inductive proofs or consistency. SMT encodings translate clauses into quantifier-free formulas via instantiation, with solvers like Z3 using them to verify theorems in knowledge representation systems, bridging propositional SAT with expressive AI logics.

Combinatorial Optimization

SAT solvers extend to by addressing variants like Maximum Satisfiability (MaxSAT) and model counting (#SAT), enabling the solution of optimization and enumeration problems in mathematics and operations research. In MaxSAT, the objective is to find a truth assignment that maximizes the number of satisfied clauses in a , generalizing the decision-based SAT problem to an optimization setting. Weighted MaxSAT further assigns non-negative weights to clauses, aiming to maximize the total weight of satisfied clauses, which allows modeling problems with varying importance of constraints. Partial MaxSAT distinguishes between hard clauses, which must all be satisfied, and soft clauses, which contribute to the objective if satisfied; this formulation is particularly useful for incorporating soft constraints in optimization scenarios, such as where some requirements can be relaxed. The problem, or model , computes the exact number of satisfying assignments for a given , providing a count rather than a single solution. This is valuable for probabilistic , where the number of models informs probability distributions over possible worlds, such as in Bayesian networks or reliability analysis. Approximate #SAT solvers trade precision for scalability on large instances, estimating counts via sampling or bounding techniques. Combinatorial problems are often solved by reducing them to SAT or its variants, leveraging efficient encodings to exploit solver strengths. For , vertices and edges are encoded as variables and clauses ensuring adjacent vertices receive different colors, with k-colorability checked via SAT; extensions to MaxSAT optimize for the minimum number of colors by iteratively tightening constraints. Set cover problems reduce to SAT by representing sets as variables and clauses that enforce coverage of all elements, while weighted MaxSAT minimizes the total cost by assigning weights to sets. The encodes paths through variables for vertex orderings and clauses prohibiting invalid transitions, solvable as SAT for existence or #SAT for counting paths in probabilistic graph models. Notable solvers include MaxHS, developed in the , which uses an implicit hitting set approach combining SAT solving with integer linear programming to efficiently handle weighted partial MaxSAT instances, achieving strong performance on industrial benchmarks. For #SAT, Cachet employs component caching integrated with DPLL-style search and clause learning, providing both exact counts and approximations through heuristic bounding for large-scale probabilistic applications. Theoretically, SAT and its variants connect to statistical physics through phenomena in random k-SAT instances, where thresholds emerge from and landscapes, inspiring algorithms like survey that model clause-variable interactions as spin glasses. These links also extend to random structures, analyzing average-case complexity via probabilistic methods to explain solver behavior on structured versus random formulas.

Performance and Modern Developments

Benchmarks and Competitions

The evaluation of SAT solvers relies on standardized benchmarks and competitions that provide rigorous testing grounds for performance improvements. Benchmark suites such as SATLIB, established in the late , offer a foundational collection of propositional instances drawn from diverse domains, including logic synthesis and combinatorial problems, enabling reproducible comparisons across solvers. Industrial benchmark suites, sourced from hardware verification, , and AI planning applications, introduce real-world complexity with large-scale instances featuring millions of clauses, reflecting practical deployment challenges. Annual SAT competitions, initiated in 2002, serve as pivotal events to benchmark solver advancements and discover challenging instances, fostering innovation in the field. These competitions feature distinct categories such as application (real-world encodings), crafted (algorithmically generated hard instances), and random/combinatorial (structured probabilistic problems), allowing targeted evaluation of solver robustness. Primary metrics include the number of solved instances within time limits, average runtime, and the PAR-2 score, which penalizes unsolved instances by assigning twice the cutoff time to emphasize both speed and coverage. For unsatisfiable instances, solvers must produce verifiable proofs, typically in DRAT (DRAT proofs) format, to certify correctness, with evaluation extending to proof size and validation efficiency using independent checkers. Reference implementations like CaDiCaL and Kissat, known for their and high performance in prior competitions, are often used as baselines for new solvers due to their clean interfaces and extensive feature sets. Recent iterations, including the SAT Competition, have emphasized parallel and distributed solving tracks to address on multi-core systems, alongside integrated evaluations for MaxSAT variants that optimize partial solutions in weighted settings. These trends highlight growing focus on distributed architectures and extensions beyond pure SAT, with results showing parallel solvers resolving approximately 6.6% more instances (370 vs. 347) than sequential baselines in the main track.

Notable Solvers and Recent Advancements

MiniSat, developed in 2004 by Niklas Eén and Niklas Sörensson, became a foundational CDCL-based SAT solver due to its simplicity, efficiency, and open-source implementation, influencing numerous subsequent solvers through its clean codebase and propagation mechanisms. Glucose, introduced in the by Audemard and Laurent Simon, advanced CDCL techniques by incorporating adaptive noise strategies, lazy evaluation, and dynamic restarts, achieving superior performance on industrial benchmarks compared to earlier solvers like MiniSat. Kissat, created by Biere and released around 2020, won the SAT 2020 main track by introducing inprocessing techniques such as transitive reduction and non-minimal learned clauses, enabling it to solve over 90% more instances than competitors on diverse problem sets. In the 2020s, distributed solving saw innovations like ManySAT, a portfolio-based parallel SAT solver that runs multiple diversified sequential configurations simultaneously, achieving superlinear speedups on multicore systems by sharing learned clauses across threads. Recent AI-driven advancements have integrated large language models (LLMs) to automate solver evolution and optimization. SATLUTION, a 2025 framework from researchers, employs LLM agents to iteratively evolve SAT solver codebases starting from 2024 competition winners, producing variants that solved 344–347 instances in the SAT Competition 2025—outperforming the human-designed winners' 334 instances—while also surpassing prior years' benchmarks without access to future data. Similarly, AutoModSAT (2025) uses LLMs to modularize complex CDCL solvers and discover novel heuristics, yielding a 50% performance improvement over baseline Kissat on diverse datasets and a 20% speedup over parameter-tuned state-of-the-art alternatives. Further AI integrations include DynamicSAT (2025), which dynamically tunes solver parameters like branching heuristics and clause activity decay during runtime based on problem characteristics, demonstrating significant gains over static configurations on the 2024 SAT Competition benchmarks. Active learning approaches for solver selection, such as those employing to predict optimal solver portfolios per instance, have also emerged, enhancing efficiency in heterogeneous environments. Looking ahead, future directions emphasize quantum-inspired methods, like encoding SAT into for faster exploration of solution spaces, and neural heuristics using graph neural networks to approximate decision-making in CDCL, potentially extending applicability to broader NP-hard problems.

References

  1. https://www.cs.cornell.edu/gomes/pdf/2008_gomes_knowledge_satisfiability.pdf
  2. https://www.cs.toronto.edu/~sacook/homepage/1971.pdf
  3. https://cacm.acm.org/research/the-silent-revolution-of-sat/
  4. https://dl.acm.org/doi/10.1145/800157.805047
  5. https://www.cs.ubc.ca/~kevinlb/papers/2021-SAT-handbook-chapter.pdf
  6. https://dl.acm.org/doi/10.1145/321033.321034
  7. https://dl.acm.org/doi/10.1145/368273.368557
  8. https://www.mcs.anl.gov/research/projects/AR/otter/
  9. https://satassociation.org/articles/FAIA185-0003.pdf
  10. https://www.sciencedirect.com/science/article/pii/S0166218X05001721
  11. https://www.cs.sfu.ca/~mitchell/papers/colLogCS85.pdf
  12. https://www.cs.cmu.edu/~emc/15-820A/reading/grasp_iccad96.pdf
  13. https://www.cs.princeton.edu/~zkincaid/courses/fall18/readings/SATHandbook-CDCL.pdf
  14. https://www.princeton.edu/~chaff/publication/DAC2001v56.pdf
  15. https://minisat.se/Papers.html
  16. https://dl.acm.org/doi/abs/10.1007/s10472-005-0424-6
  17. https://www.cs.helsinki.fi/u/mjarvisa/papers/jarvisalo-leberre-roussel-simon.aimag.pdf
  18. https://www.cs.ubc.ca/~hoos/Publ/ubc-99-06.pdf
  19. https://ojs.aaai.org/aimagazine/index.php/aimagazine/article/view/2450/2358
  20. https://dl.acm.org/doi/10.1007/s10601-012-9121-3
  21. https://www.cs.cmu.edu/~15414/s22/lectures/14-sat-dpll.pdf
  22. https://www.princeton.edu/~chaff/publication/iccad2001_final.pdf
  23. https://www.cs.cornell.edu/gomes/pdf/1998_gomes_aaai_iaai_boosting.pdf
  24. https://lara.epfl.ch/w/_media/projects:minisat-anextensiblesatsolver.pdf
  25. https://www.cs.utexas.edu/~marijn/publications/cube.pdf
  26. https://content.iospress.com/articles/journal-on-satisfiability-boolean-modeling-and-computation/sat190070
  27. https://fmv.jku.at/papers/HeisingerFleuryBiere-SAT20.pdf
  28. https://www.cs.cmu.edu/~mheule/publications/distributed-LRAT.pdf
  29. https://hal.science/hal-01540785v1/document
  30. https://journals.sagepub.com/doi/10.3233/SAT190063
  31. https://arxiv.org/abs/2511.07737
  32. https://satcompetition.github.io/2025/satcomp25slides.pdf
  33. https://www.cs.cornell.edu/selman/papers/pdf/92.aaai.gsat.pdf
  34. https://web2.qatar.cmu.edu/~gdicaro/15281/additional/dimacs93-walksat.pdf
  35. https://www.cs.ubc.ca/~hoos/Publ/jar00.pdf
  36. https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/AAAI96-177.pdf
  37. https://ieeexplore.ieee.org/document/4211988
  38. https://ojs.aaai.org/index.php/AAAI/article/view/33228
  39. https://www.cs.cmu.edu/~emc/papers/Papers%20In%20Refereed%20Journals/Bounded%20Model%20Checking%20Using%20Satisfiablility%20Solving.pdf
  40. https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/Equivalence_Checking_11_30_08.pdf
  41. https://abs.informatik.uni-freiburg.de/papers/2007/DS_2007.pdf
  42. http://www.kroening.com/papers/dac2003.pdf
  43. https://www.sciencedirect.com/science/article/pii/S0747717102000913
  44. https://www.cs.utexas.edu/~hunt/FMCAD/fmcad11/papers/8.pdf
  45. https://ofers.dds.technion.ac.il/publications/sat14.pdf
  46. https://www.cs.cornell.edu/selman/papers/pdf/92.ecai.satplan.pdf
  47. https://www.ijcai.org/Proceedings/95-2/Papers/080.pdf
  48. https://www.cs.cornell.edu/selman/papers/pdf/99.ijcai.blackbox.pdf
  49. https://ml.rwth-aachen.de/~hector.geffner/www.dtic.upf.edu/~hgeffner/hlp-caepia05.pdf
  50. https://jair.org/index.php/jair/article/download/10618/25394/19742
  51. https://research.tue.nl/files/199807615/Janssen_G.pdf
  52. https://www.sciencedirect.com/science/article/pii/S157106610800296X
  53. https://www.cs.utexas.edu/~isil/cs389L/maxsat-handouts.pdf
  54. https://www.cs.toronto.edu/~jdavies/Davies_Jessica_E_201311_PhD_thesis.pdf
  55. https://www.cs.cornell.edu/~sabhar/chapters/ModelCounting-SAT-Handbook-prelim.pdf
  56. https://www.cs.cmu.edu/~ckingsf/bioinfo-lectures/sat.pdf
  57. https://homes.cs.washington.edu/~beame/papers/cachet-heuristics.pdf
  58. https://arxiv.org/abs/cond-mat/0406217
  59. https://upcommons.upc.edu/bitstreams/a251ea45-708c-4979-8fb7-c0a7f0f5edb9/download
  60. https://satcompetition.github.io/
  61. https://ojs.aaai.org/aimagazine/index.php/aimagazine/article/download/2395/2278
  62. https://github.com/satcompetition/template
  63. https://www.cs.cmu.edu/~mheule/publications/p01c15-prf.pdf
  64. https://link.springer.com/chapter/10.1007/978-3-031-65627-9_7
  65. https://satcompetition.github.io/2024/
  66. https://maxsat-evaluations.github.io/2024/
  67. https://satcompetition.github.io/2024/results.html
  68. https://www.sciencedirect.com/science/article/pii/S0004370221001235
  69. https://www.researchgate.net/publication/220163323_ManySAT_a_parallel_SAT_solver
  70. https://arxiv.org/abs/2509.07367
  71. https://arxiv.org/abs/2507.22876
  72. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.34
  73. https://ml-for-solvers.github.io/
  74. https://www.researchgate.net/publication/319339569_Solving_SAT_and_MaxSAT_with_a_Quantum_Annealer_Foundations_and_a_Preliminary_Report
Add your contribution
Related Hubs
User Avatar
No comments yet.