返回
摘要
En 中文
The past decade has seen clause learning as the most successful algorithm for SAT instances arising from real-world applications. This practical success is accompanied by theoretical results showing clause learning as equivalent in power to resolution. There exist, however, problems that are intractable for resolution, for which clause-learning solvers are hence doomed. In this paper, we present extended clause learning, a practical SAT algorithm that surpasses resolution in power. Indeed, we prove that it is equivalent in power to extended resolution, a proof system strictly more powerful than resolution. Empirical results based Oil an initial implementation suggest that the additional theoretical power can indeed translate into substantial practical gains. (c) 2010 Elsevier B.V. All rights reserved.
Keyword:
SAT
Clause learning
Resolution
AI总结
对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。
期刊
IF:
13.9
论文数:
6.1K
被引数:
1.9W
机构
引用论文
Electron density imaging of protein films on gold-particle surfaces with transmission electron microscopy
Cytometry
IF0
Peripheral nerve injury differentially regulates dopaminergic pathways in the nucleus accumbens of rats with either ‘pain alone’ or ‘pain and disability’
Neuroscience
IF0

