Extended Clause Learning

Dr Jinbo Huang (NICTA and ANU)

COMPUTER SCIENCE SEMINAR Logic and Computation

DATE: 2010-09-07
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

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.
BIO:
Dr Huang is a senior researcher at NICTA (Managing Complexity Research Group), with an adjunct appointment in the School of Computer Science at the Australian National University. His research interests include logical and probabilistic reasoning and their applications, and artificial intelligence in general. He completed his PhD in 2005 in the Computer Science Department at the University of California, Los Angeles as a member of the Automated Reasoning Group.