Content area
In this thesis, we introduce a strongly polynomial combinatorial algorithm for feasibility checking in a Horn constraint system (HCS) that is also certifying. Study of HCS is important as they have numerous applications in logic programs, econometrics, program verication and lattice optimization. The algorithm described here is certifying in that it does provide an easily checkable certicate, in the event that the input HCS is deemed infeasible. The running time of the algorithm is O(m : n2) where m is the number of constraints and n is the number of variables in the system. More precisely, we are interested in certifying algorithms for system:
Ax ≥ b; x ≥ 0; min Σnj=1 xj
where A is a m × n matrix whose elements &epsis; {−1; 0; 1}. In addition we will assume that each row of A has at most one +1. Such systems are called Horn Constraint Systems (HCS for short). If in addition, each row has at most one −1, the system is called a Dierence Constraint System (DCS for short). DCS systems arise in the context of shortest path problems in graph algorithm literature. While it is possible to solve these using linear programming techniques, such algorithms are not guaranteed to be combinatorial. In[4] and [5] a "lifting" algorithm was discussed and this is a combinatorial polynomial time algorithm but not certifying when the problem is not feasible; when the problem is feasible, the solution itself acts as a certicate to verify that this solution is the optimal solution. In case we have a DCS system, both the lifting algorithm and Bellman-Ford algorithm are combinatorial strongly polynomial time algorithms that are also certifying. Here we discuss an extension of Bellman-Ford algorithm for HCS which is combinatorial, strongly polynomial time, and certifying. This work also shows how the lifting algorithm may be turned into a certifying algorithm.