Institution: Stanford University, Department of Computer Science

Title: An $n^{log n}$ algorithm for the two-variable-per-constraint linear programming satisfiability problem

Author: Nelson, Charles Gregory

Date: November 1978

Abstract: A simple algorithm is described which determines the satisfiability over the reals of a conjunction of linear inequalities, none of which contains more than two variables. In the worst case the algorithm requires time O(${mn}^{\lceil \log^2 n \rceil + 3}$), where n is the number of variables and m the number of inequalities. Several considerations suggest that the algorithm may be useful in practice: it is simple to implement, it is fast for some important special cases, and if the inequalities are satisfiable it provides valuable information about their so1ution set. The algorithm is particularly suited to applications in mechanical program verification.

http://i.stanford.edu/pub/cstr/reports/cs/tr/78/689/CS-TR-78-689.pdf