West Virginia University

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.

Friday, November 14, 2008

3:30 p.m.

Wean Hall 8220

Principles
of Programming Seminars