提出了一种基于总和器编码的伪布尔约束通用编码方法（GTE），该方法不依赖系数的数量，且在大伪布尔约束中表现优越，同时在无此特征的约束下也具有竞争力。

Jul, 2015

布尔可满足性 (SAT) 是一个基础的 NP-complete 问题，具有许多应用，包括自动计划和调度。为了解决大规模的情况，SAT 求解器必须依赖启发式算法，如在 DPLL 和 CDCL 求解器中选择一个分支变量。我们建议使用机器学习模型来改进这些启发式算法，通过减少步数来降低运行时间，但是由于有用的模型相对较大和较慢，这通常会阻碍运行时间。我们建议首先使用训练好的机器学习模型进行几个初始步骤，然后将控制权交给经典启发式算法，这简化了 SAT 求解的冷启动，并可以减少步数和总运行时间，但需要单独决定何时将控制权交给求解器。此外，我们介绍了一种改进的 Graph-Q-SAT，专门针对从其他领域转换而来的 SAT 问题，例如开放式车间调度问题。我们通过随机和工业 SAT 问题验证了我们方法的可行性。

Jul, 2023

该研究论文主要研究了基于二元决策图的 Pseudo-Boolean 约束编码技术，提出了使用系数分解方法克服爆炸性增长问题，并给出了第一个多项式广义弧一致的 ROBDD 编码算法。

Jan, 2014

本文综述了近期文献，重点介绍了利用机器学习技术来解决布尔可满足性问题（SAT）的方法，包括从基于手工特征的朴素分类器到最新的端到端 SAT 求解器 NeuroSAT，以及将现有的 CDCL 和本地搜索求解器与机器学习相结合的最新进展。总体而言，利用机器学习解决 SAT 是一个有前途但充满挑战的研究课题，文章指出了当前研究的局限性并提出了未来可能的方向。

Mar, 2022

应用深度学习解决困难的组合问题具有巨大的潜力。该研究侧重于布尔可满足性（SAT）问题，并通过基本的概率方法消除了由于训练集仅限于小于实际问题规模几个数量级的随机公式导致的难题。使用我们的生成器，我们对现有的最先进模型进行训练，以预测具有 10,000 个变量的公式的可满足性，提出了新的分类器，可以对大多数困难水平的相同数据集进行显着改进，从而打破了过去基于公式的句法特征学习的方法，并使用求解器计算的简短前缀进行学习。

Nov, 2022

通过引入双变量来解决逻辑连接约束的快捷方式问题，将编码形式化为与模型的原始训练损失兼容的分布损失，实现学习逻辑约束的新框架在模型的普适性和约束满足方面表现出卓越的性能。

Mar, 2024

该研究提出了一种基于整数规划和强化学习算法的统一框架 DCSAT，用于解决不同类型的布尔可满足性问题，包括 MaxSAT、Weighted MaxSAT、PMS 和 WPMS 等。通过调整目标函数系数，构建了统一的整数规划表示方法，并基于 0-1 整数规划构建了适当的强化学习模型。基于二叉树搜索结构，在 SAT 问题上应用了蒙特卡罗树搜索（MCTS）方法，证明了该方法能够基于维纳 - 欣钦大数定律找到所有最优的布尔赋值。实验证明，该方法能够剪枝不必要的搜索空间，找到问题的最优布尔赋值，同时为 SAT 问题的监督学习方法提供多样的标签。

Dec, 2023

本文提出了一种用于从数据中挖掘约束条件的一般框架，该框架以整数线性规划问题的形式考虑结构化输出预测中的推断，然后通过估计可行集的外部和内部多面体来挖掘底层约束条件，并在各种合成和现实应用中验证了所提出的约束挖掘算法。

Jun, 2020

本论文提出并提供了多种自然理论公式的有效算法，以解决在学习多个不同目标函数时，学习者可共享某些未知公共特征的问题，并且可以学习到捕捉这种共性的新的内部表示，以便更高效地学习和使用更少的数据。

Nov, 2014

利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

Sep, 2023