A Fully Polynomial Time Approximation Scheme for Refutations in Weighted Difference Constraint Systems

This paper is concerned with the design and analysis of approximation algorithms for the problem of finding the least weight refutation in a weighted difference constraint system (DCS). In a weighted DCS (WDCS), a positive weight is associated with each constraint. Every infeasible DCS has a refutation, which attests to its infeasibility. The length of a refutation is the number of constraints used in the derivation of a contradiction. Associated with a DCS \(\mathbf{D}\) is its constraint network \(\mathbf{G}\). \(\mathbf{D}\) is infeasible if and only if \(\mathbf{G}\) has a simple, negative cost cycle. It follows that the shortest refutation of \(\mathbf{D}\) corresponds to the length of the shortest negative cost cycle in \(\mathbf{G}\). The constraint network of a WDCS is represented by a constraint network, where each edge contains both a cost and a positive, integral length. In the case of a WDCS, the weight of a refutation is defined as the sum of the lengths of the edges corresponding to the refutation. The problem of finding the minimum weight refutation in a WDCS is called the weighted optimal length resolution refutation (WOLRR) problem and is known to be NP-hard. In this paper, we describe a pseudo-polynomial time algorithm for the WOLRR problem and convert it into a fully polynomial time approximation scheme (FPTAS). We also generalize our FPTAS to determine the optimal length refutation of a class of constraints called Unit Two Variable per Inequality (UTVPI) constraints.