定义 B = {0, 1} 和一个布尔函数 f p : B N → B，其中 p 是 B n中的布尔参数向量。假设 f p (x) 可以表示为一个布尔表达式，其变量是向量 p 和 x 的元素。假设 c 是计算 f p (x) 的成本，该成本以某种方式衡量，例如，基于某些完整的布尔运算符集的运算符求值次数。那么，给定 B 中的 y 和 B N中的 x，使用最简单的暴力搜索，求解方程 f p (x) = y 以满足 y 的成本为c2n 。
对于 3SAT 求解，已知一个更好的最坏情况界限，即 O(1.307 n )，参见此处，相关讨论参见此处。对于定义不精确的“工业问题”，实践中的表现通常要好得多；相关讨论参见此处。
现在考虑一组布尔特征向量 x i和标签 y i ，其中 i 在 {1, …, d} 区间。现在可以求解 f p (x i ) = y i ，其中 i 为所有 i。由于待求解的未知变量数量保持不变，因此计算成本的简单界限为 cd² n ，与数据值数量 d 呈线性关系。需要注意的是，如果所讨论的现象可以用少量逻辑参数 n 建模，则计算成本很容易处理。
在实践中，机器学习问题通常不会精确求解，而是近似求解，即最小化损失函数。可以使用类似 Z3 的 SAT 求解器中的AtLeast运算符，要求至少有 K 个i值满足 f p (x i ) = y i ，其中 K 为某个值。然后，可以通过对 K 进行二分运算来找到最大的 K，这需要 log 2 (d) 个这样的 SAT 解。关于此问题的精确求解器，另请参见此处。
AtLeast 运算符可以通过二进制加法器/加法器编码（ Bailleux 和 Boufkhad 2003 ）、顺序计数器编码（ Sinz 2005 ）或 Batcher 排序网络方法（ Abío 等人 2013 ）来实现。遗憾的是，所有这些方法都需要添加大量辅助变量，从而对朴素复杂度界限产生不利影响。然而，我们可以希望，对于工业问题，性能会比这个界限好得多，就像实践中经常出现的情况一样。此外，已知在多项式时间内运行的随机近似算法可以证明找到满足可满足布尔约束的最大数量的保证分数（例如，3/4 或更多）的分配（例如，参见这里、这里、这里和这里）。这可以作为精确求解优化器的代理。
如果问题具有布尔表达式，其中嵌入了有界范围的整数变量的线性不等式谓词，则可以使用上面描述的想法直接应用 SMT 求解器方法，或者将问题转换为 SAT 问题并直接应用上述方法。
以本文所述方式使用 SAT 求解器进行机器学习的想法可以追溯到 ( Kamath 等人，1992 )。该方法在 Donald Knuth 的 TAOCP 可满足性分册的“学习布尔函数”一节中通过示例进行了描述。
通过可满足性解决进行机器学习的文章最先出现在John D. Cook身上。
原文： https://www.johndcook.com/blog/2025/07/31/machine-learning-by-satisfiability-solving/