Maximum satisfiability (MAX SAT) problem is an optimization version of
the satisfiability (SAT) problem. This problem arises in certain appl
ications in expert systems and knowledge base revision. MAX SAT proble
m is NP-hard. Some algorithms can solve this problem, but they are not
adapted to the special cases where the number dr 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 anot
her instance P of which the number of variables is smaller than the nu
mber 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 o
f T. Therefore, this algorithm is an efficient preprocessing step.