A Certifying Algorithm for Linear (and Integer) Feasibility in Horn Constraint Systems

In this paper, we discuss a certifying version of the Lifting Algorithm for Horn constraint systems. Recall that a Horn constraint system (HCS) is a specialized polyhedral system that finds application in a number of domains such as program verification (abstract interpretation) and operations research. HCSs are closely related to Leontief substitution systems. In previous work, it was established that the problem of checking if a Horn polytope is non-empty is polynomial time solvable. However, that algorithm is not certifying in that if the input HCS is infeasible, it does not provide a certificate which attests to the infeasibility of the HCS. Consequently, the output provided by an implementation of the algorithm is not trustworthy. Trustworthiness is an integral aspect of AI systems. The current paper rectifies this issue by modifying the lifting algorithm to make it certifying. In particular, both “yes”-instances and “no”-instances of input HCSs will be certified through appropriate Farkas’ variables. However, the increased trustworthiness of the algorithm comes at a cost; the new algorithm is less efficient than its non-certifying counterpart.