Kirk Boyer, College of Charleston


A Geometric Algorithm for Linear Constraint Satisfiability

Abstract: The applications of solving linear boolean satisfiability problems (linear SAT) extend from computability problems to electronic design automation. A linear SAT can be represented by a coefficient matrix C, a variable vector x, and a right-hand-side vector b. The goal is to determine whether there exists an x such that Cx >= b and as a possibly separate task, find such an x. I present an algorithm that takes advantage of the geometry of such problems to find x if it does exist. By treating each linear constraint as a half-space defined by the hyperplane which is the level curve of a linear function, the algorithm follows the gradients of these functions toward the intersection of the corresponding half-spaces. This intersection contains all points that satisfy all constraints, and thus all solutions to the linear SAT. This algorithm can be used to find an initial feasible solution to a linear programming problem for use with Simplex Search or other optimization algorithms.

Mentor: Amy Langville (College of Charleston)