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

  • Shaohan Ma
  • Dongmin Liang


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. LetT be any instance of the MAX SAT problem. The algorithm transformsT into another instanceP of which the number of variables is smaller than the number of clauses ofT. Using other algorithms, the optimal solution toP can be found, and it can be used to construct the optimal solution ofT. Therefore, this algorithm is an efficient preprocessing step.


MAX SAT problem bipartite graph independent set complexity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Eiter, T., Gottlob, G., On the complexity of propositional knowledge base revision, updates, and counterfactuals,Artificial Intelligence, 1992, 57: 227.MATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Andrasfai, B.,Introductory to Graph Theory, Budapest and Adam Hilger: Bristol, 1977.Google Scholar
  3. 3.
    Hopcroft, J. E., Karp, R. M., Ann 5/2 algorithm for maximum matching in bipartite graphs,SIAM J. Comput., 1973, 2: 225.MATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Ma Shaohan,Algorithms for Graphs (in Chinese), Guizhou: Guizhou People's Press, 1988.Google Scholar

Copyright information

© Science in China Press 1997

Authors and Affiliations

  • Shaohan Ma
    • 1
  • Dongmin Liang
    • 1
  1. 1.Department of Computer ScienceShandong UniversityJinanChina

Personalised recommendations