许多计算机科学中的组合问题都可以被归为检验命题语句的可满足性。对可满足性算法的任何改进对于处理复杂性的能力都有巨大的作用。
完备的回溯算法
戴维斯-普特南算法，得名于马丁·戴维斯和希拉里·普特南的重要论文。这个算法实际上采用的是戴维斯、洛吉曼和洛夫兰所描述的版本，因此使用所有 4 位作者姓氏的首字母$DPLL$命名这个算法。
$DPLL$使用一个合取范式形式（即一个子句集）的语句作为输入。类似于回溯搜索和真值表枚举算法，它本质上是递归地、深度优先地枚举可能的模型。$DPLL$算法是一种搜索算法，思想与$DFS$十分相似，或者说$DPLL$算法本身就属于$DFS$的范畴，它将搜索所有可能的赋值排列。
具体地说，$DPLL$算法会在公式中选择一个变量（命题变号），将其赋值为 $True$，化简赋值后的公式，如果简化的公式是可满足的（递归地判断），那么原公式也是可满足的。否则就反过来将该变量赋值为$False$，再执行一遍递归的判定，若也不能满足，那么原公式便是不可满足的。这被称为分离规则，因为其将原问题分离为了两个更加简单的问题。
它在真值表枚举算法的基础上进行了 3 项改进：
提前终止：算法可以用部分完成的模型来检测语句是否必然为真或为假。如果任一文字为真则子句为真，即使其他文字还没有真值；这样，整条语句在模型完成之前就可以断定其真值。类似地，若任一子句为假，即其所有文字为假，则语句为假。同样，这种情形可能会在模型完成前很久就发生。提前终止避免了在搜索空间中检查全部子树。
纯符号启发式方法：纯符号是指在所有子句中“符号位”（正负文字）都相同的符号。易知如果一条语句有模型，则存在一个模型对纯符号的赋值使其文字为真，因为这样做不会使子句为假。注意，在确定符号是否为纯时，算法可以忽略当前已构建的模型中已知为真的子句。
单元子句启发式方法：之前对单元子句的定义是只有一个文字的子句。在$DPLL$中，它也指那些除了一个文字外，其余文字都被模型赋值为$false$的子句。单元子句启发式方法在余下的部分出现分支前对所有这样的符号赋值。这种启发式的一个重要结果是，所有对知识库中的已有文字进行的证明（通过反证法）将立刻得证。还要注意的是，对一个单元子句赋值可能会创建另一个单元子句，这种强制赋值的“级联”被称为单元传播。这类似于确定子句的前向链接。实际上，如果$CNF$表达式仅含有确定子句，则$DPLL$本质上复制了前向链接。
$SAT$求解器能够用于大规模问题的技巧实际上都很寻常，在之前已经见过它们的其他形式：
（1）分量分析：当$DPLL$为变量赋真值时，子句集可能会被分割成不相交的子集，称之为分量，它们没有共同的未赋值变量。给定一个高效探测这一状况的方法，求解器就可以通过对每个分量独立求解来加快速度。
（2）变量排序与值排序：对$DPLL$的简单实现使用任意的变量顺序，并在赋值时总是先尝试赋真再尝试赋假。度启发式算法建议在所有剩余子句中优先选择最常出现的变量。
（3）智能回溯：许多用按时序回溯几小时都求解不了的问题，如果改用智能回溯直接回溯到导致冲突的相关点上，那么问题可以在几秒内求解。所有运用智能回溯的$SAT$求解器都使用冲突子句学习的某种形式来记录冲突，以避免在后续的搜索中重复出现。通常只保留有限大小的冲突集，丢弃极少使用的冲突。
（4）随机重启：有时单次运行似乎无法取得进展。此时，可以从搜索树的顶端重新开始，而非尝试继续搜索。重启后对变量和值选取进行不同的随机选择。第一次运行中学习到的子句在重启后依然被保留，这有助于对搜索空间进行剪枝。重启并不保证能更快地找到解，但它能够减小求解时间的方差。
（5）聪明索引：$DPLL$和其他现代求解器用到的加速方法需要快速索引“$X_i$作为正文字出现的子句集合”。这一任务相当复杂，因为算法所感兴趣的只是先前的变量赋值尚未满足的子句，因此索引结构必须在计算过程中动态更新。
有了这些改进，现代求解器可以处理有数千万个变量的问题。它们为诸如硬件验证和安全协议验证这样的领域带来革命性的变化。在此之前，这些领域需要十分费力的、手动证明。
局部搜索算法
只要选择了正确的评价函数，局部搜索算法可就以被直接用于可满足性问题。由于目标是找出满足所有子句的赋值，一个对未满足的子句进行计数的评价函数就可以胜任这项工作。实际上，这正是用于$CSP$的$Min$-$Conflict$算法所使用的量度。这些算法都在完全赋值的空间采取动作，每次只翻转一个符号的真值。这个空间通常含有许多局部极小值，要跳出这些极小值，需要各种形式的随机方法。近年来，人们进行了大量实验，试图在贪婪性与随机性之间找到一个良好的平衡。
这些算法中最为简单和有效的算法之一是$WalkSAT$。算法每次循环都选择一个未满足的子句，并在该子句中选择一个符号来翻转。选择要翻转的符号的方法有两种：（1）最小化新状态中未满足子句的数量的“最小冲突”方法；（2）随机挑选一个符号的“随机游走”方法。算法随机选取一种。
当$WalkSAT$返回一个模型时，输入语句就是可满足的。但当它返回$failure$时，则有两种可能的原因：语句不可满足，或需要多给算法一些时间。如果我们设定足够大的时间限制，$WalkSAT$最终将返回一个模型（如果存在的话），因为随机游走步骤终将遇到一个解。如果时间限制为无穷大，而语句不可满足，则算法永远不会终止！
因此，当预计问题有解的时候，$WalkSAT$最为有用。但是，$WalkSAT$并不总是能检测到不可满足性，而对判定蕴含来说这是必备的。例如，$wumpus$世界中，一个智能体不能使用$WalkSAT$来可靠地证明一个方格是安全的。不过，它可以说：“我思考了一小时，都想不出存在一种这个方格不安全的可能世界。”这也许是个不错的经验性指示，表明方格是安全的，但它绝对不是一种证明。
