Polynomial-Time 0-1 Linear Programming Approach to CNF-SAT Using Totally Unimodular Matrices
Angelo Monfroglio *
Alumni PoliMi, Politecnico di Milano, and MIUR, Italy.
*Author to whom correspondence should be addressed.
Abstract
Efficient 0-1 Linear Programming Approach for CNF-SAT Based on Unimodularity.
CNF-SAT, i.e, the satisfaction of a Conjunctive Normal Form, is considered of NP complexity. It can be formulated as an Integer Programmining problem. This short paper presents a 0-1 Linear Programming relaxation which solves CNF-SAT in polynomial time. Main novel contribution is that the structure of the A matrix for the Simplex algorithm guaranties that the solution is always integer, because the matrix is totally unimodular. Thus, this result is important from the comlexity point of view. CNF-SAT is the model of several very important practical constraint satisfaction problems in the real life. The work has strong implications for both theoretical research and practical applications involving constraint satisfaction problems in computer science and operations research.
Keywords: Conjuctive normal form satisfaction, integer programming, 0-1 linear programmig, simplex, unimodularity, complexity, python