Dag-Like Unit Refutations in UTVPI Constraint Systems
摘要
In this paper, we investigate the problem of finding the shortest dag-like unit refutation of a system of Unit Two Variable Per Inequality (UTVPI) constraints. Unit refutations in difference constraints (both tree-like and dag-like) have been studied in the literature. Unit refutations are important from the perspective of identifying restrictions on variables which cause inconsistencies. They are also useful from the perspective of visualizing the cause of inconsistency in a constraint system. Unit resolution refutations form the backbone of logic programming engines. Here, we investigate unit refutations in polyhedral constraint systems. In particular, our focus is on optimal length dag-like unit refutations. Previous research has established that this problem is NP-hard. In the current work, we design a pseudo-polynomial time algorithm and an approximation algorithm for this problem. It is unusual for a problem to be both APX-complete and solvable in pseudo-polynomial time.