使用 MaxSAT 优化二进制决策图以进行分类

AAAIMar, 2022

使用 MaxSAT 优化二进制决策图以进行分类

Optimizing Binary Decision Diagrams with MaxSAT for classification

Hao Hu, Marie-José Huguet, Mohamed Siala

TL;DR本文提出了基于 SAT 的方法学习最优二元决策图（BDD），以更好地实现可解释的机器学习模型，并给出了一种整合兼容子树的方法，该方法与现有方法相比在预测质量和可解释性方面具有明显的优势。

Abstract

The growing interest in explainable artificial intelligence (XAI) for critical decision making motivates the need for interpretable machine learning (ML) models. In fact, due to their structure (especially with small sizes), these models are inherently understandable by humans. Recentl

interpretable machine learning binary decision diagrams sat-based models maxsat model prediction quality

发现论文，激发创造

MORBDD：多目标受限二进制决策图的稀疏学习

通过机器学习方法，本研究使用二进制决策图在多准则决策中精确求解多目标整数线性规划问题，发现适用于单目标问题的局限二进制决策图可通过 ML 方法进行改进，产生具有优秀近似精度且规模较小的稀疏解。

Mar, 2024

伪布尔约束的 BDDs 新视角

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

Jan, 2014

MLIC: 一种基于 MaxSAT 的学习可解释分类规则的框架

该论文介绍了一个名为 MLIC 的 MaxSAT 框架，用于搜索适用于命题逻辑的可解释分类规则，并演示了它在解决包含数万个示例和数千个特征的大型分类问题方面的有效性和可调节的准确性与可解释性之间的平衡。

Dec, 2018

SAT 问题的机器学习：约束启发式和新的图表示

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

Jul, 2023

DeepSAT: 一种基于 EDA 驱动的 SAT 学习框架

提出了 DeepSAT 框架，使用 EDA 领域的知识来解决布尔可满足性问题（Boolean satisfiability），通过逻辑合成算法将 SAT 实例预处理为优化的与非图（AIGs），并利用 DAGNN 训练条件生成模型，在各种 SAT 实例上实现了显著的准确度提高。

May, 2022

使用 SATNet 学习可靠的逻辑规则

通过可区分性学习生成可解释和可验证的逻辑规则，该方法通过最大可满足性求解器（SATNet）学习可解释的逻辑规则，并引入验证技术进行验证，从而实现了逻辑推理和深度学习的交互。

Oct, 2023

句子决策图的相对简洁性

本文旨在确定哪些布尔函数可以由小型的 SDDs 表示，同时将多项式大小的布尔函数表示集合与来自 Darwiche 和 Marquis 经典知识编译地图的表示类型进行比较。最主要的结果是通过等效的不明确的非确定性 OBDDs 对 SDDs 进行准多项式仿真，回答了 SDDs 和超过 OBDDs 的 FBDDs 相对简洁性之间的一个开放问题。

Feb, 2018

SDDs 比 OBDDs 更为简洁

本文介绍了一种名为 sentential decision diagrams (SDDs) 的表达语言，证明了在布尔函数的表示中 SDDs 比 ordered binary decision diagrams (OBDDs) 更简洁，该结论解决了知识编译中的一个开放性问题，并且在人工智能和知识编译等领域有广泛的应用。

Jan, 2016

一种基于增量最大可满足性问题的平衡规则学习模型

提出了一种基于 MaxSAT 的增量学习可解释和平衡规则的模型 IMLIB，并通过与 IMLI 在多个数据库上的比较表明，IMLIB 在准确性上与 IMLI 相当，生成尺寸更小且更平衡的规则。

Mar, 2024

可解释分类规则的高效学习

本文介绍了一种名为 IMLI 的基于最大可满足性的可解释学习框架，通过结合小批量学习和迭代规则学习的方法，实现了分类规则的合成。实验结果表明，IMLI 在预测准确性、可解释性和可伸缩性之间取得了最好的平衡，并用于学习流行的可解释分类器，如决策列表和决策集。

May, 2022