EFFICIENT ALGORITHMS FOR CERTAIN SATISFIABILITY AND LINEAR PROGRAMMING PROBLEMS

We present efficient algorithms for certain cases of Linear Equations solving, Linear Programming, and SATisfiability testing. The LP problem is Turing equivalent to solving Linear Inequalities (LI), where one simply asks whether a given set of linear inequalities has a solution or not. LE, LP, and SAT have all been studied in both the theoretical and the applied areas of Computer Science. Although many algorithms have been developed for these problems, there are large gaps between today's best algorithms and the best theoretical lower bounds.;In the algorithms for LE(2) and LI(2), we associate an undirected graph with a given instance. Vertices correspond to variables; edges are labelled by equations "ax + by = c" or inequalities "ax + by (LESSTHEQ) c", respectively. In the SAT algorithm, we associate a directed graph with a given instance. Vertices correspond to variables and their negations, and there is a directed edge from u to v if and only if there is a clause u (V) v.;For LE(2), if we know that x = p, we can transfer this value over the edge and obtain y = (c - ap)/b from the equation ax + by = c. A decision at one end of an edge forces a decision at the other. We show how to transfer the value of one variable to another by performing a search on the graph, and further, how to obtain the initial value x = p.;For 2-SAT, if we know that the variable x must be true in the clause x (V) y, we cannot conclude anything about y from the clause; but if x is false, then y must be true if the Boolean expression is to be satisfied. In the graph we have the corresponding edges x (IMPLIES) y and y (IMPLIES) x. If x and x are in the same strong component, then we can derive x (IMPLIES) x (IMPLIES) x and the Boolean expression is not satisfiable. We show that if no variable x appears in the same strong component as its negation x, then the Boolean expression is satisfiable. We generalize our method to testing the truth of Quantified Boolean Formulas in 2-CNF.;We do not eliminate these gaps, but instead present efficient algorithms for LE, LI, and SAT for the cases in which there are at most two variables or literals per "unit" (equation, inequality, or clause). The algorithms for LE(2) and 2-SAT are linear-time algorithms, and they are optimal except for constant factors. Our algorithm for LI(2) has a non-linear worst-case time bound, but the bound is better than the bound of any general LI algorithm such as the polynomial-time algorithm by Khachiyan. The subcases discussed seem to be in some sense the "hardest" ones that are not as hard as the general problems; i.e., for LE, LI, and SAT, there seems to be a difference in complexity when going from two to three variables or literals per "unit".;If a Boolean expression in CNF is restricted to at most one negated variable per clause, then the expression can be tested for satisfiability in linear time; but for CNF expressions restricted to at most two negated variables per clause, SAT is NP-complete. We call a CNF expression a disguised NR(1) expression if it can be mapped to an equivalent CNF expression with at most one negated variable per clause by replacing certain variables by their negations everywhere. We show that disguised NR(1) expressions can be identified in linear time by using the 2-SAT algorithm.;The most important of the problems we discuss is LI(2). If we know that ax > a(xi) in any solution, we obtain from an edge inequality "ax + by (LESSTHEQ) c" the bound by (LESSTHEQ) c - a on y. Bounds can be transferred from variable to variable using a graph search. We guess values for the variables; if a guess is not feasible, we can derive more restrictive bounds from the inequalities labelling a loop in the graph. A binary search technique allows us to find a feasible value x = (xi) if one exists. The overall running time is polynomial in the size of the input, and the algorithm seems to be of practical as well as theoretical importance.