Computational Logic Seminar
Date and Time: Thursday March 11, 2004 @ 1:30pm
Place: ASB 9705
Speaker: Joey Hwang
Title: Resolution Proof Complexity of Constraint Satisfaction
Abstract:
Constraint Satisfaction problems (CSPs) arise in a variety of applications including
artificial intelligence, scheduling, machine vision, molecular biology, graph
coloring, and circuit design. This leads to a strong motivation to develop efficient
algorithms to solve CSPs.
A simple approach is to perform backtracking to directly search for solutions. We will describe 2 versions of this approach: backtracking with d-way branching (BT) and backtracking with 2-way branching (2BT). BT is more natural and is studied in most papers in the literature. 2BT is implemented in some commercial solvers such as Ilog and Eclipse. It has been proven that 2BT is super-polynomially more powerful than BT. The main goal in our research is to improve the seperation from super-polynomial to exponential.
Two resolution-based proof systems will be studied in the talk. We will explain how they are related to the two backtracking algorithms and how we improve the above seperation by showing there is an exponential seperation between the two proof systems.