K. Subramani
West Virginia University

Optimal length resolution refutation for difference constraints

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

Principles of Programming Seminars