A linear-time transformation of linear inequalities into conjunctive normal form
We present a technique that transforms any binary programming problem with integral coefficients to a satisfiability problem of propositional logic in linear time. Preliminary computational experience using this transformation, shows that a pure logical solver can be a valuable tool for solving binary programming problems. In a number of cases it competes favourably with well known techniques from operations research, especially for hard unsatisfiable problems.
|Department of Computer Science [CS]|
Warners, J.P. (1996). A linear-time transformation of linear inequalities into conjunctive normal form. Department of Computer Science [CS]. CWI.