Optimal
length resolution refutation for
difference constraints
Abstract:
This
talk is concerned with determining the optimal length
resolution refutation (OLRR) of a system of difference constraints
over an integral domain. The problem of finding short explanations
for unsatisfiable Difference Constraint Systems (DCS) finds
applications in a number of design domains including program
verification, proof theory and real-time scheduling and Operations
Research. It is well-known that resolution refutation is a sound and
complete procedure to establish the unsatisfiability of boolean
formulas in clausal form. The literature has also established that a
variant of the resolution procedure called Fourier-Motzkin
elimination is a sound and complete procedure for establishing the
unsatisfiability of Linear Constraint Systems (LCS). Our work
first establishes that every DCS has a short (polynomial
in the size of the input) resolution refutation and then shows that
there exists a polynomial time algorithm to computes the optimal
size refutation. One of the consequences of our work is that the
Minimum Unsatisfiable Subset (MUS) of a DCS can be computed in
polynomial time; computing the MUS of an unsatisfiable constraint
set is an extremely important aspect of certifying algorithms.
Host: Frank
Pfenning
Appointments:
Frank
Pfenning <fp@cs.cmu.edu>
Friday, November
14, 2008 3:30 p.m.
Wean
Hall 8220