L’archive ouverte pluridisciplinaire HAL, estdestinée au dépôt et à la diffusion de documentsscientifiques de niveau recherche, publiés ou non,émanant des établissements d’enseignement et derecherche français ou étrangers, des laboratoirespublics ou privés.0HAL Id: tel-040042130https://theses.hal.science/tel-04004213v20提交日期：2023年2月24日0HAL是一个多学科的开放获取存储库，用于存储和传播科学研究文档，无论其是否已发表。这些文档可能来自法国或国外的教育和研究机构，也可能来自公共或私人研究中心。0通过最大布尔可满足性实现可解释的机器学习模型0Hao Hu0引用此版本：0Hao Hu. 通过最大布尔可满足性实现可解释的机器学习模型. 计算机科学中的逻辑 [cs.LO].图卢兹国家应用科学学院, 2022. 英文. �NNT : 2022ISAT0035�. �tel-04004213v2�En vue de l’obtention duDélivré par :l’Institut National des Sciences Appliquées de Toulouse (INSA de Toulouse)École doctorale et spécialité :MITT : InformatiqueUnité de Recherche :Laboratoire d’Analyse et d’Architecture des Systèmes (LAAS-CNRS)Directeur(s) de Thèse :Marie-José Huguet et Mohamed SialaRapporteurs :Chu-Min Li et Frédéric Koriche0THÈSE THÈSE0图卢兹大学博士学位0于2022年12月14日提交和答辩：Hao Hu0通过最大布尔可满足性实现可解释的机器学习模型0评审委员会：Hélène Fargier研究主任，评审委员会主席；FrédéricKoriche教授，评审委员会成员；Chu-Min Li教授，评审委员会成员；DjamalHabet教授，考官；Marie-José Huguet教授，博士导师；Mohamed Siala副教授，博士导师0世界上只有一种英雄主义，那就是在认清生活真相后，还依然热爱它。0（罗曼∙罗兰—《米开朗基罗传》, 1907）0（罗曼∙罗兰—《米开朗基罗传》,1907）0世界上只有一种英雄主义，那就是在认清生活真相后，还依然热爱它。0There is only one heroism in the world: tosee the world as it is, and to love it.0（罗曼∙罗兰—《米开朗基罗传》, 1907）0Il n’y a qu’un héroïsme au monde: c’est de voir le monde tel qu’ilest, et de l’aimer.0世界如此，要去爱它。0（罗曼∙罗兰—《米开朗基罗传》, 1907）0ii0致谢0作为论文的最后一部分，致谢部分自然被认为是最容易的。然而，就个人而言，由于其特殊的里程碑属性，它并不容易。似乎很多事件就发生在昨天：我大学入学考试的失败，第一次接触计算机科学，与我的未婚妻的相识，第一次到达法国的日子，决定攻读计算机科学博士学位，新冠疫情，论文答辩...生活不是一次排练，但它确实留下了许多偶然但美好的记忆，与许多最初的陌生人。首先，我衷心感谢我的博士导师：Marie-JoséHuguet教授和MohamedSiala副教授。我永远不会忘记与他们一起在可解释的机器学习模型研究上的合作时光。Marie-Jo的认真和勤奋的教学和研究态度对我产生了永久的影响。作为一名外国学生，我感谢他们在我日常生活中的理解和关心，尤其是在新冠疫情期间。我特别感谢法国国家科学研究中心的研究员EmmanuelHebrard，他为我提供了在LAAS-CNRS的研究实习机会。我感谢他允许我自由探索自己的研究兴趣，这激发了我博士论文的研究课题。同时，我要对所有评委们表示衷心的感谢：Chu-Min Li教授，Frédéric Koriche教授，Hélène Fargier教授和DjamalHabet教授。感谢你们阅读我的论文。特别是对于Chu-Min和Frédéric，我感谢他们在答辩中宝贵的意见和亲自到场。我要感谢ROC小组的所有同事，他们对我都非常友善和温柔。此外，我感谢法国高等教育、研究和创新部（MESRI）提供给我三年的博士合同，以及LAAS-CNRS的接待。我要感谢许多以前的朋友和老师。曹瑞哲，我们在欧洲有很多共同的旅游经历。我很怀念我们在阿尔卑斯山度过的那段时光，也希望你在杭州工作顺利。徐涛副教授，感谢你对我博士申请和我在西北工业大学的学术职位的帮助。我期待与你未来的合作。此外，我还要感谢在图卢兹认识的许多朋友。吴振航博士，感谢你和你的建议，我们有很多讨论，就像兄弟一样。我希望你在米其林上海工作顺利。毛宇晓博士，感谢你在研究中的许多讨论，帮助我释放研究压力。我希望你在波尔多工作顺利。陈彤博士，在一个特殊的时期，我们是LAAS-CNRS唯一的两个中国人，我感谢你在日常生活中的支持，还有你可爱的猫。我希望你能尽快找到一个完美的博士后职位。刘星瀚，一个疯狂但是假的阿森纳球迷，我感谢你对我解决经济困境的支持。祝你今年年底的答辩顺利，还有你的羽毛球技术。还要非常感谢其他人：方凯0iii0薛光杰，张超，任树立，王树立，任泰伟，徐刚，黄刚等，以及那些在ENAC一起打羽毛球的朋友们。特别是，我要感谢在INSAToulouse的所有中国学生。感谢你们给我提供了成为助教的机会，让我感受到了教学的辛苦和快乐。这些教学经验将对我未来成为一名真正的讲师有很大帮助。我真诚希望你们所有人在接下来的几年里顺利通过所有考试并毕业。此外，我还要感谢西北工业大学，那是我获得本科教育和未来学术职位的地方。此外，我还要感谢“粉红之城”图卢兹。在我看来，这是欧洲最宜居的城市，因为它具有包容的社会和热情的人民。最后，也是最重要的，我要对我的父母和未婚妻耿子琛表示极大的感激。在开始我的本科教育之后，我的父母一直尊重我的选择，并尽力在精神和经济上支持我继续深造。如果来自父母的无私支持是因为血缘关系，那么来自未婚妻的支持只能是因为爱情。我们在2016年相爱，并在我去法国之前只在一起度过了11个月。尽管有时你抱怨分离的困难，但你总是支持我的决定。在过去的5年里，我在你的生活中主要是缺席的，我唯一能做的就是从现在开始填补你未来的生活，直到我的生命结束。0HaoHu，图卢兹，2023年2月14日。0iv0摘要0由于对现代人工智能系统所做关键决策背后的推理理由的理解日益关注，可解释机器学习模型受到越来越多的关注。由于其结构，特别是在小规模情况下，这些可解释模型对人类来说是易于理解的。与传统的启发式方法相比，最近的精确方法提供了更紧凑的模型或更好的预测质量。在本论文中，我们提出了两种基于最大布尔可满足性（MaxSAT）的新颖精确方法，用于学习最优的可解释机器学习模型。0我们的贡献始于一种基于最大布尔可满足性（MaxSAT）的原始精确方法，用于学习最优决策树。该方法通过优化经验准确性来避免过拟合，并丰富约束以限制树的深度。此外，我们将这种基于MaxSAT的方法集成到AdaBoost中，AdaBoost是一种经典的Boosting方法，用于提高泛化性能。实验结果显示，与最先进的启发式方法和其他精确方法相比，这种基于MaxSAT的方法具有竞争力的预测质量。在集成到AdaBoost后，预测性能明显改善。我们的第二个贡献是一种基于最大布尔可满足性（MaxSAT）的原始精确方法，用于优化二进制决策图。我们引入了一个初始的布尔可满足性（SAT）编码，以在有限深度下模拟二进制决策图，并实现了如何将基于SAT的模型调整为MaxSAT方法。最后，我们提出了一种预处理方法，用于选择一些重要特征，以提高我们基于MaxSAT的方法优化二进制决策图的可扩展性。实验结果显示，与最先进的启发式方法相比，我们的基于MaxSAT的方法在预测质量上取得了明显的进步。在编码大小和模型大小之间，我们的方法与最先进的精确方法相比，不会损失预测性能。此外，在应用预处理后，编码大小大大减小，提高了可扩展性。0关键词：可解释机器学习，最大布尔可满足性，决策树，决策图。v0摘要0Interpretable learning models are receiving increasing interest due to growingconcerns for understanding the reasoning behind crucial decisions made bymodern artificial intelligence systems. Due to their structure, especially for smallsizes, these interpretable models are inherently understandable to humans.Compared to traditional heuristic methods for learning these models, recent exactmethods offer more compact models or achieve better prediction quality. In thisthesis, we propose two new exact methods based on Maximum BooleanSatisfiability (MaxSAT) to learn optimal interpretable learning models.0Our contribution begins with an original exact method based on MaxSAT to learnoptimal decision trees. This method optimizes empirical accuracy to avoidoverfitting and also takes constraints into account to restrict the depth of the tree.In addition, we integrate this MaxSAT-based method into the AdaBoost method,which is a standard boosting method to improve generalization performance.Experimental results show competitive prediction quality of this MaxSAT-basedmethod compared to heuristic and exact methods from the state of the art.Furthermore, prediction performance improvements are observed after integrationinto AdaBoost. Our second contribution is an original exact method based onMaxSAT to optimize binary decision diagrams. We first introduce a BooleanSatisfiability (SAT) encoding to model limited-depth binary decision diagrams withperfect accuracy. Then, we present how to adapt the model into MaximumBoolean Satisfiability. Finally, we present a preprocessing for selecting certainimportant features to increase the scalability of our MaxSAT method foroptimizing binary decision diagrams. Experimental results show advances of ourMaxSAT method on prediction quality compared to heuristic methods. We alsoobserve significant reduction in encoding size and model size in comparisonsbetween our approach and an exact method from the state of the art, withoutlosing prediction performance. Moreover, a large reduction in encoding size ishighlighted after applying the preprocessing, which enhances scalability.0关键词：可解释学习，最大布尔可满足性，决策树，决策图。0目录0引言 101 形式背景和现有技术 501.1 SAT和MaxSAT问题 . . . . . . . . . . . . . . . . . . . . . . . 601.1.1 布尔可满足性 . . . . . . . . . . . . . . . . . . . . . . . 601.1.2 最大布尔可满足性 . . . . . . . . . . . . . . . . 801.2 机器学习 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1001.2.1 基础知识 . . . . . . . . . . . . . . . . . . . . . . . . . 1001.2.2 可解释的机器学习模型 . . . . . . . . . . . . 1401.2.3 集成方法 . . . . . . . . . . . . . . . . . . . . . . . . 2001.3 可解释的机器学习模型的相关工作 . . . . . . . . . . . . . . 2501.3.1 决策树的相关方法 . . . . . . . . . . . . . . 2501.3.2 决策图的相关方法 . . . . . . . . . . . . . 3202 通过MaxSAT学习最优决策树 3902.1 动机和问题描述 . . . . . . . . . . . . . . . . . . . 4002.2 先前SAT编码的细节 . . . . . . . . . . . . . . . . . . . 4102.2.1 编码给定大小的有效二叉树 . . . . . . . . . . 4102.2.2 将特征和类别映射到节点 . . . . . . . . . . . . 4302.2.3 将所有示例正确分类 . . . . . . . . . . . . . . . 4402.3 提出的MaxSAT模型 . . . . . . . . . . . . . . . . . . . 4602.3.1 最大化正确分类的示例 . . . . . . . . . . . . . . . 4702.3.2 控制给定大小的树的深度 . . . . . . . . . . . . 4902.3.3 在给定区间内限制树的大小 . . . . . . . . . . . . . . 5102.4 实验结果 . . . . . . . . . . . . . . . . . . . . . . . . . . . 5302.4.1 过拟合现象 . . . . . . . . . . . . . . . . . . 5302.4.2 与不同方法的比较 . . . . . . . . . . . . . . 5502.5 提升模型 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5702.5.1 集成在AdaBoost中 . . . . . . . . . . . . . . . . . . . . 5802.5.2 实验结果 . . . . . . . . . . . . . . . . . . . . . . 5902.6 不同MaxSAT求解器的性能 . . . . . . . . . . . . . . . . 5902.6.1 不完全加权轨道 . . . . . . . . . . . . . . . . . . 6102.6.2 不完全加权轨道 . . . . . . . . . . . . . . . . . . . 640第二章总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6403 通过MaxSAT优化二进制决策图 6703.1 动机和问题描述 . . . . . . . . . . . . . . . . . . . . . . . . . . . 6703.2 一个重要命题 . . . . . . . . . . . . . . . . . . . . . . . . . 6903.3 提出的SAT和MaxSAT模型 . . . . . . . . . . . . . . . . . . 7203.3.1 初始SAT模型：BDD 1 . . . . . . . . . . . . . . . . . . . 720第八章 内容03.3.2 第二个SAT模型：BDD 2 . . . . . . . . . . . . . . . . . . . 7703.3.3 第三个SAT模型：BDD 3 . . . . . . . . . . . . . . . . . . . 8003.3.4 MaxSAT转换 . . . . . . . . . . . . . . . . . . . . 8203.3.5 合并兼容的子树 . . . . . . . . . . . . . . . . . . 8203.4 实验结果 . . . . . . . . . . . . . . . . . . . . . . . . . . . 8303.4.1 不同SAT编码的比较 . . . . . . . . . . . . . . . . . . . . 8403.4.2 与现有启发式方法的比较 . . . . . . . . . . . . . 8703.4.3 与精确决策树方法的比较 . . . . . . . . . . . . . . . . . . . 9103.5 启发式MaxSAT模型 . . . . . . . . . . . . . . . . . . . . . . . 9403.6 章节总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . 960结论和未来工作 990附录 1030过拟合现象的详细结果 1050B 学习最优决策树和提升树的基准描述 1110C 扩展摘要 1150C.1 引言 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1150C.2 通过MaxSAT优化的最优决策树并集成到Ad- aBoost中 . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . 116 C.2.1 提出的MaxSAT模型 . . . . . . . . . . . . . . . . . . . . 1180C.2.2 实验 . . . . . . . . . . . . . . . . . . . . . . . . . 1210C.3 通过MaxSAT优化的最优二进制决策图 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .122 C.3.1 提出的SAT和MaxSAT模型 . . . . . . . . . . . . . . . . 1230C.3.2 实验0参考文献0引言0在过去的十年中，机器学习在解决许多现实世界问题方面取得了巨大成功。这些成功增加了可解释人工智能（XAI）的发展，特别是对于高风险决策系统。XAI旨在产生人类可以理解的AI系统。其目标是通过理解导致特定决策或预测的过程来提高人类对AI系统的信任。XAI领域涵盖了广泛的研究范围。在本论文中，我们对机器学习模型的可解释性感兴趣。在文献中，有两种主要方法可以增加机器学习模型的可解释性。第一种称为事后方法，专注于黑盒模型，如神经网络或深度学习，并考虑事后解释[ Guidotti et al. 2018]。可以对黑盒模型的输出进行解释，以详细说明给定预测的原因，或者对黑盒进行检查以解释给定黑盒的工作原理。在第二种透明度设计方法中，目标是基于其简单结构，产生人类可以理解的机器学习模型。例如，当决策树、决策集或决策规则的大小较小时，它们被认为是可解释的设计模型。[ Rudin 2019 , Laugel et al. 2019]中强调了黑盒解释方法的一些缺点，可能提供误导性或错误的解释。对于可能影响个体的关键应用程序，这些缺点引发了对固有可解释机器学习模型的需求。[ Rudin et al. 2021]详细介绍了固有可解释机器学习模型开发的十个挑战。第一个挑战涉及如何高效计算最优稀疏的机器学习模型。本论文与此挑战保持一致。对于可解释的机器学习模型，存在许多启发式方法。尽管这些经典的启发式方法减少了计算时间，但构建的可解释的机器学习模型通常非常庞大，使得难以理解模型的工作原理。为了确保找到的机器学习模型真正“可解释”，最近对这些模型的精确方法越来越感兴趣。与启发式方法相比，精确方法在模型大小、模型深度或准确性方面提供了最优性的承诺。在这种情况下，组合优化方法，如约束编程、混合整数线性规划、布尔可满足性（SAT）和动态规划，已成功应用于学习最优可解释的机器学习模型。这些声明性方法特别有趣，因为它们在学习模型时提供了一定的灵活性。在本论文中，我们重点研究了最大布尔可满足性（MaxSAT）方法，其中MaxSAT是SAT的优化版本，用于学习最优可解释模型。最近SAT-based精确方法的一个缺点是对于给定的模型大小或模型深度，承诺完美的经验准确性，这可能导致过拟合。然而，基于MaxSAT的精确方法可以通过优化经验准确性来避免这个缺点。此外，MaxSAT具有加权扩展，其中子句的权重可以自然地近似于机器学习中使用的数据集的数据分布。此优势还使得基于MaxSAT的精确方法易于在Boosting方法中进行调整。02 引言0我们提供了论文的概述，其中包含三个章节。第1章0论文概述0我们提供了论文的概述，其中包含三个章节。第1章0介绍了布尔可满足性的技术背景，包括布尔可满足性（SAT）及其变种最大布尔可满足性（MaxSAT）。然后，介绍了机器学习中的重要概念，包括可解释模型和集成方法。最后，第1章对解释性机器学习模型的最新相关工作进行了文献综述，包括经典的启发式方法和最近的精确方法。第2章介绍了我们在通过MaxSAT学习最优决策树及其在AdaBoost中的集成方面的贡献。第3章介绍了我们在通过MaxSAT优化二进制决策图方面的贡献。我们对本论文的贡献进行了总结。01. 通过MaxSAT学习最优决策树及其在AdaBoost中的集成作为一种非常流行的机器学习模型，决策树因其固有的可解释性和广泛的高效启发式方法而受益。然而，由于树的规模和深度的爆炸性增长，由经典启发式方法找到的决策树在可解释性方面存在困难。这个弱点促使了精确方法来学习最优决策树，在某些度量指标（如树的大小、树的深度和准确性）上具有数学最优性的保证。一些精确方法是基于SAT的，其中[Bessiere et al. 2009 , Narodytska et al. 2018]优化树的大小，而[Avellaneda 2020 , Janota & Morgado 2020]优化树的深度。然而，所有这些方法都必须满足决策树在训练集上的完美准确性的约束，这经常被批评为可能导致过拟合。0为了弥补这个缺点，我们首先引入了一种MaxSAT方法来通过优化准确性学习最优决策树，这是之前SAT方法的改进[ Narodytska et al. 2018]。首先，我们介绍了之前的SAT编码的细节，并展示了如何将SAT编码转化为MaxSAT以优化准确性。然后，我们提出了新的约束来限制深度。接下来，为了提高预测质量，我们通过调整软子句的权重将MaxSAT方法集成到AdaBoost中。0根据大量的实验结果，我们观察到之前的SAT方法存在过拟合现象。此外，我们观察到在AdaBoost中集成后的预测性能具有竞争力。30与最先进的启发式方法和精确方法相比，我们提出的MaxSAT方法在性能上表现出明显的改进。此外，在AdaBoost集成后，我们观察到预测质量明显提高。02. 通过MaxSAT优化二进制决策图二进制决策图作为对布尔函数提供紧凑表示的方法，在二元分类中被视为可解释性的。与决策树相比，有序简化的二进制决策图可以有效地避免复制问题和碎片化问题[Oliver 1992 , Kohavi 1994]，这是决策树所遭受的两个主要缺陷。据我们所知，目前唯一一种学习最优二进制决策图的精确方法是[Cabodi et al. 2021]，其目标是具有最小尺寸且能正确分类所有示例的二进制决策图。然而，这个目标导致了两个缺点。第一个缺点是可能由于完美准确性而导致过拟合。第二个缺点是缺乏深度限制，使得学习到的二进制决策图尺寸小但深度较大成为可能。0为了避免这些缺点，我们提出了一种基于MaxSAT的方法来学习深度受限的二进制决策图，并具有最佳的经验准确性。首先，我们引入了一个初始的基于SAT的模型，以完美的准确性对给定深度的二进制决策图进行编码。然后，我们将SAT模型提升到MaxSAT以优化准确性。此外，由于MaxSAT编码的复杂性与相应的SAT编码密切相关，我们提出了另外两个基于SAT的模型，目标相同但编码尺寸更紧凑。最后，为了增加所提出的MaxSAT方法的可扩展性，我们提出了一个混合版本，通过启发式方法选择重要特征的子集，然后应用所提出的MaxSAT方法。0我们的实验评估比较了我们的MaxSAT方法与最先进的启发式方法和精确方法之间的差异。首先，与启发式方法相比，我们的MaxSAT方法在预测质量上具有明显优势。然后，与精确方法（学习最优决策树的MaxSAT方法）相比，我们的MaxSAT方法在编码大小和模型大小上显示出明显的缩小。同时，我们的MaxSAT方法显示出竞争性的预测性能。最后，混合版本在报告最优性方面比原始版本更容易，但在预测质量上仍然具有竞争力。0出版物0本论文中介绍的工作已发表在两个国际会议上。这些出版物详见第2章和第3章。0• 使用MaxSAT学习最优决策树及其在AdaBoost中的集成。Hao Hu，MohamedSiala，Emmanuel Hébrard，Marie-José04 引言0Huguet. 在第二十九届国际人工智能联合会议（IJCAI2020）论文集中，第1170-1176页。[Hu等人，2020]0• 使用MaxSAT优化二进制决策图进行分类。Hao Hu，Marie-JoséHuguet，Mohamed Siala。在第三十六届AAAI人工智能大会（AAAI2022）论文集中，第3767-3775页。[Hu等人，2022]0我们很荣幸地看到学习最优决策树的MaxSAT公式被选为MaxSAT评估2021年[Bacchus等人，2021a]和2022年[Bacchus等人，2022]的基准。基准的描述详见附录A。0• 学习最优决策树和提升树的基准描述。Hao Hu，Emmanuel Hébrard，Marie-JoséHuguet，MohamedSiala。在MaxSAT评估2021年论文集中，第39-40页。[Hu等人，2021]0我们还在两个法语会议上介绍了关于使用MaxSAT优化二进制决策图的工作：JFPC2022（Journées Franco- phones de Programmation par Contraintes）和CNIA2022（Conférence Nationale en Intelligence Artificielle）。0第1章形式背景和最新技术0目录01.1 SAT和MaxSAT问题 . . . . . . . . . . . . . . . . . . . 601.1.1 布尔可满足性 . . . . . . . . . . . . . . . . . . . . . . . 601.1.2 最大布尔可满足性 . . . . . . . . . . . . . . . . 801.2 机器学习 . . . . . . . . . . . . . . . . . . . . . . . . . 1001.2.1 基本知识 . . . . . . . . . . . . . . . . . . . . . . . . . 1001.2.1.1 分类和回归 . . . . . . . . . . . . . . 1001.2.1.2 评估指标 . . . . . . . . . . . . . . . . . . . 1101.2.2 可解释的机器学习模型 . . . . . . . . . . . . 1401.2.2.1 决策树 . . . . . . . . . . . . . . . . . . . . . 1401.2.2.2 二进制决策图 . . . . . . . . . . . . . . . 1701.2.2.3 其他模型 . . . . . . . . . . . . . . . . . . 1901.2.3 集成方法 . . . . . . . . . . . . . . . . . . . . . . . . 2001.2.3.1 组合方法 . . . . . . . . . . . . . . . 2101.2.3.2 提升方法 . . . . . . . . . . . . . . . . . . . . . . . . 2201.2.3.3 Bagging和随机森林 . . . . . . . . . . . . . 2401.3 可解释的机器学习模型相关研究 . . . . . . . . . 2501.3.1 决策树的相关方法 . . . . . . . . . . . . . . 2501.3.1.1 传统启发式算法 . . . . . . . . . . . . 2501.3.1.2 最新的精确方法 . . . . . . . . . . . . . . . . 2901.3.2 决策图的相关方法 . . . . . . . . . . . . . 3201.3.2.1 决策图 . . . . . . . . . . . . . . . . . . . . 3201.3.2.2 OODG的启发式方法 . . . . . . . . . . . . . 3301.3.2.3 最新的精确方法 . . . . . . . . . . . . . . . . 360在本章中，我们介绍布尔可满足性（SAT）和最大布尔可满足性（MaxSAT）问题的技术背景和最新方法。第1.1节介绍了布尔可满足性（SAT）和最大布尔可满足性（MaxSAT）问题。第1.2节介绍了监督机器学习，并重点介绍了可解释机器学习和集成方法。第1.3节提供了可解释机器学习模型的最新相关工作的文献综述。具体而言，它包含了关于决策树和决策图的最新方法。0第1章 正式背景和最新技术01.1 可满足性和最大可满足性问题0布尔可满足性（SAT）问题旨在确定布尔公式是否可满足。SAT问题在计算机科学中具有关键作用，特别是因为它是第一个被证明为NP完全的问题。在本节中，我们按照[Biere等人，2021年]的标准术语，形式上描述了命题逻辑中的一些相关概念。此外，我们还描述了本论文中考虑的最大布尔可满足性问题（MaxSAT）。01.1.1 布尔可满足性0原子x是一个命题（即布尔）变量。文字p要么是原子x，称为正文字，要么是其否定¬x，称为负文字。文字p为真当且仅当p为正且其原子被赋值为1，或者p为负且其原子被赋值为0。否则，文字p为假，即¬p为真。子句c是文字的析取（p1 ∨ ∙ ∙ ∙ ∨pk）。我们假设子句中的所有文字两两不同，并且文字p和¬p不出现在同一个子句中。如果子句中至少有一个文字p（p∈c）为真，则子句c为满足。相反，如果子句中的文字都不为真，则子句c为不满足。由子句c1∧ ∙ ∙ ∙ ∧cn表示的命题公式称为合取范式（CNF）。CNF公式对应于SAT实例。SAT问题的目标是确定CNF公式的可满足性。目标是找到满足公式中所有子句的所有文字的赋值（公式被满足或简称为“SAT”）；或者报告找不到这样的赋值（公式不满足或简称为“UNSAT”）。有几种完整的算法可以解决SAT问题。最古老的方法之一是Davis-Putnam-Logemann-Loveland（DPLL）算法[ Davis等，1962年]。大多数现代SAT求解器中应用的最新方法是冲突驱动子句学习（CDCL）算法[Silva＆Sakallah 1996 ， Silva＆Sakallah 1999 ， Moskewicz等，2001年 ，Eén＆Sörensson 2003年]。在DPLL算法中，通过搜索树来探索搜索空间，其中每个节点对应于限制搜索空间的决策（分支变量选择和值赋值）。搜索树以深度优先搜索（DFS）方案进行探索。当检测到“UNSAT”时，回溯到最后一个节点。然后，反转最后的决策并恢复探索。这种回溯称为时间回溯。在探索过程中，每个搜索树节点执行两个步骤：搜索和传播。搜索步骤与启发式方法相关，涉及分支变量选择和值赋值，以探索搜索结构。一些经典的启发式方法包括纯随机选择和最小大小子句的最大出现次数（MOM）[ Zabih＆McAllester 1988 ， Silva1999 ]。传播步骤与剪枝死胡同分支有关。DPLL算法使用一种01.1. 可满足性和最大可满足性问题70一种叫做单元传播(Unit-propagation,UP)的传播类型，在两种可能的条件下触发。第一种条件是当一个子句c只有一个未赋值的文字p（c被称为单元子句）时，UP强制令c中的p为true，因为这是使c满足的唯一方式。第二种条件是当一个子句c被已赋值的文字不满足时，UP直接返回公式的“UNSAT”。我们在算法1
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
