Extended clause learning
Date
2010
Authors
Huang, Jinbo
Journal Title
Journal ISSN
Volume Title
Publisher
Elsevier
Abstract
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 on an initial implementation suggest that the additional theoretical power can indeed translate into substantial practical gains.
Description
Keywords
Keywords: Clause learning; Empirical results; Proof system; Real-world application; Resolution; SAT; SAT instances; Theoretical result; Learning algorithms Clause learning; Resolution; SAT
Citation
Collections
Source
Artificial Intelligence
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description