【IJCAI 2019】使用SAT Oracles计算（Computing with SAT Oracles），Joao Marques-Silva，Alexey Ignatiev

报告主题： Computing with SAT Oracles

简介：

命题可满足性（SAT）是计算机科学的一个成功案例。冲突驱动子句学习(CDCL)范式是大多数最先进的SAT解决方案的基础，它的力量使它们成为一种不可替代的选择工具，适合于高效地解决工业问题。事实上，SAT求解器可以被视为生成NP-oracle的见证，它可以应用于求解NP之外的决策问题，但也可以超越NP，例如在多项式层次的更高层次中，以及函数和枚举问题。

本教程的任务是全面概述现代SAT求解技术以及如何利用SAT求解器解决约束问题，解决SAT的扩展和推广（即在处理优化和枚举问题时）。此外，本教程还将重点介绍如何将SAT解算器作为oracles应用于各种战略实际应用，从图形优化问题、基于模型的诊断到协作路径查找以及机器学习模型的验证和解释。本教程将问题编码的细节汇集到SAT、最大和最小可满足性（Max SAT／MISAT）、最小不可满足性（MUS计算）、量化布尔公式（QBF）中，而且还针对前述问题提出基于SAT的高效算法。

邀请嘉宾：

Joao Marques-Silva是图卢兹大学ANITI的研究主席，研究兴趣包括自动推理、人工智能和机器学习。在加入ANITI之前，曾就读于都柏林大学学院(IE)，南安普顿大学(英国)，里斯本大学(PT)。在ANITI，是深度学习者解释和验证的研究主席。

Alexey Ignatiev是里斯本大学理学院信息学(DI)理性实验室的研究员。在此之前是里斯本大学(University of Lisbon) 的博士后研究员，研究与SAT Oracles计算和推理相关的各种课题以及其它许多问题领域。目前研究主要集中在发展和完善高效的SMT-based(可满足性模理论)决策和优化过程中针对各种重要的实际应用人工智能:从软件包升级能力和布尔公式最小化基于模型的诊断(MBD),软件故障定位和可辩解的AI(新品)。