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...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.