A polynomial-time algorithm for reducing the number of variables in MAX SAT problem

Maximum satisfiability (MAX SAT) problem is an optimization version of the satisfiability (SAT) problem. This problem arises in certain applications in expert systems and knowledge base revision. MAX SAT problem is NP-hard Some algorithms can solve this problem, but they are not adapted to the special cases where the number of variables is larger than the number of clauses. Usually, the number of variables has great impact on the efficiency of these algorithms. Thus, a polynomial-time algorithm is proposed to reduce the number of variables. Let T be any instance of the MAX SAT problem. The algorithm transforms T into another instance P of which the number of variables is smaller than the number of clauses of T. Using other algorithms, the optimal solution to P can be found, and it can be used to construct the optimal solution of T. Therefore, this algorithm is an efficient preprocessing step.