A Scalable Weighted Max-SAT Implementation of Propositional Etcetera Abduction
A Scalable Weighted Max-SAT Implementation of Propositional Etcetera Abduction
复制标题
DOI：
--
复制
发表时间：
2017-05
期刊：
影响因子：
--
通讯作者：
Naoya Inoue;A. Gordon
中科院分区：
文献类型：
--
作者：
Naoya Inoue;A. Gordon
溯因推理或最佳解释推理技术的最新进展，鼓励将溯因法应用于现实生活中的常识性推理问题。本文描述了Etcetera溯因法，这是一种基于概率论并使用当代线性规划求解器进行优化的逻辑溯因法的新实现。我们提出了加权Max-SAT公式等绑架，这使我们能够利用在SAT和运筹学领域开发的高度先进的技术。我们的实验证明了我们的建议在包含多达一万个公理的大规模合成基准上的可扩展性，使用了在这些领域开发的最先进的数学优化器之一。这是第一个在这个尺度上评估基于sat的溯因推理方法的工作。我们开发的推理引擎已经公开了。
Recent advances in technology for abductive reasoning, or inference to the best explanation, encourage the application of abduction to real-life commonsense reasoning problems. This paper describes Etcetera Abduction, a new implementation of logical abduction that is both grounded in probability theory and optimized using contemporary linear programming solvers. We present a Weighted Max-SAT formulation of Etcetera Abduction, which allows us to exploit highly advanced technologies developed in the field of SAT and Operations Research. Our experiments demonstrate the scalability of our proposal on a large-scale synthetic benchmark that contains up to ten thousand axioms, using one of the state-of-the-art mathematical optimizers developed in these fields. This is the first work to evaluate a SAT-based approach to abductive reasoning at this scale. The inference engine we developed has been made publicly available.