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

Jan, 2014

本文探讨机器学习分类器编译成布尔电路同样具有输入-输出行为，定义二进制分类器决策背后的决策原因，并阐述其在应用层面的影响。此外，还提出了“充分的”，“必要的”和“完整的”决策原因的概念，以及对分类器和决策偏差的定义。根据这些概念，我们提出了高效的算法，并使用案例研究来论证它们的实用性。

Feb, 2020

本文证明了求出随机森林的一个PI解释是D^P完全的，并提出了一种命题编码方法，以使用SAT求解器找到PI解释。实验结果表明，该SAT方法的效果显著优于现有的启发式方法。

May, 2021

本文研究布尔决策树在导出、最小化和计数足够原因和对比解释方面的计算能力，证明了给定决策树的实例的最小大小的所有足够原因集合可以指数级大于输入大小，因此生成完整的足够原因集合可能是不可行的，而生成一个足够原因集无法证明是充分的，介绍了相关特征和必要特征的概念以及解释重要性的概念，并展示了如何通过一个模型计数操作获取特征重要性和足够原因的数量，最后表明，与足够的理由不同，决策树给定实例的所有对比解释可以在多项式时间内导出、最小化和计数。

Aug, 2021

本篇论文研究用于决策树的最小的delta相关集的计算方法，提出两种用于计算决策树最小的delta相关集的逻辑编码并设计一个多项式时间复杂度的算法，并且实验结果表明这些计算方法是实用的。

May, 2022

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

Nov, 2022

研究了基于决策可分离负范式电路的布尔函数主要子句的枚举问题EnumIP，将其归纳于枚举复杂度的框架内，并证明它在OutputP与IncP中。此外，研究了两个更具挑战性的限制问题，其中一个是关于表示部分最小诱导解释的子句的问题，另一个则涉及到了可解释人工智能领域中的重要概念 - 具有合理原因的主要子句，最后还提供了一些可行性证据。

Jan, 2023

研究基于电路复杂度的先验模型，并使用它们来学习部分信息中的布尔函数。该模型假设，布尔函数或布尔字符串由一些电路的贝叶斯混合生成。在电路复杂度方面表现良好。

Jun, 2023

通过使用监督式机器学习方法，探讨选择伪布尔约束和线性约束的编码问题，我们展示了使用标准特征集和专门设计的特征集可以有效地选择编码，甚至对于未见过的问题类别也能取得良好的结果，相比使用相同特征集的AutoFolio结果有优势。我们讨论了实例特征对选择最佳编码任务的相对重要性，并比较了多种机器学习方法的变体。

Jul, 2023

我们的研究提出了解释决策树的符号化语言ExplainDT，它基于我们称之为StratiFOILed的一阶逻辑构建的精心构造的片段。StratiFOILed在表达能力和评估复杂度上保持平衡，能够计算许多事后解释，包括局部解释（例如归纳和对比解释）和全局解释（例如特征相关性），同时仍处于布尔NP层次结构之上。此外，StratiFOILed查询可以写成NP问题的布尔组合，因此我们可以通过调用一次SAT求解器对其进行实际评估。在理论方面，我们的主要贡献是对StratiFOILed的表达能力和评估复杂度进行深入分析；在实践方面，我们提供了一种对StratiFOILed查询进行编码的优化实现，并对其效率进行了实验研究。

Oct, 2023