In this paper, we present variable minimal unsatisfiability (VMU), which is a generalization of minimal unsatisfiability (MU). A characterization of a VMU formula F is that every variable of F is used in every resolution refutation of F. We show that the class of VMU formulas is D P -complete. For fixed deficiency (the difference of the number of clauses and the number of variables), the VMU formulas can be solved in polynomial time. Furthermore, we investigate more subclasses of VMU formulas. Although the theoretic results on VMU and MU are similar, some observations are shown that the extraction of VMU may be more practical than MU in some cases.


Polynomial Time Model Check Conjunctive Normal Form Propositional Formula Quadratic Time 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    McMillan, K.L., Amla, N.: Automatic Abstraction Without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Gupta, A., Ganai, M., Yang, Z., Ashar, P.: Iterative Abstraction using SAT-based BMC with Proof Analysis. In: Proceedings of International Conference on Computer-Aided Design (ICCAD 2004), pp. 416–423 (2004)Google Scholar
  4. 4.
    Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Proceedings of Formal Methods in Computer Aided Design (FMCAD 2002). LNCS, vol. 2517, pp. 33–51. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Li, B., Wang, C., Somenzi, F.: A Satisfiability-Based Approach to Abstraction Refinement in Model Checking. In: Proceedings of Bounded Model Checking (BMC 2003). ENTCS, vol. 89(4) (2003)Google Scholar
  6. 6.
    Li, X., Li, G., Shao, M.: Formal Verification Techniques Based on Boolean Satisfiability Problem. Journal of Computer amd Technology 20, 38–47 (2005)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Kleine Büning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  8. 8.
    Zhao, X.: Complexity Results on Minimal Unsatisfiable Formulas-A Survey. In: Proceedings of the 9th Asian Logic Confernece, Novosbirsk, Russia (2005) (to appear)Google Scholar
  9. 9.
    Papadimitriou, C.H., Wolfe, D.: The Complexity of Facets Resolved. Journal of Computer and System Science 37, 2–13 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Kleine Büning, H.: On Subclasses of Minimal Unsatisfiable Formulas. Discrete Applied Mathematics 197(1-3), 83–98 (2000)CrossRefGoogle Scholar
  11. 11.
    Fleischner, H., Kullmann, O., Szeider, S.: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable diffierence. Theoretical Computer Science 289(1), 503–516 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Kleine Büning, H., Zhao, X.: The Complexity of Some Subclasses of Minimal Unsatisfiable Formulas, submitted for publicationGoogle Scholar
  13. 13.
    Kleine Büning, H., Xu, D.: The complexity of homomorphisms and renamings for minimal unsatisfiable formulas. Annals of Mathematics and Artificial Intelligence 43(1), 113–127 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Kleine Büning, H., Zhao, X.: Extension and equivalence problems for clause minimal formulae. Annals of Mathematics and Artificial Intelligence 43(1), 295–306 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Bruni, R., Sassano, A.: Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae, Electronic Notes in Discrete Mathematics vol. 9 (2001)Google Scholar
  16. 16.
    Y. Oh,M. N. Mneimneh, Z. S. Andraus, K. A. Sakallah, and I. L. Markov. AMUSE: A Minimally-Unsatisfiable Subformula Extractor. In Proceedings of the Design Automation Conference (DAC 2004), ACM/IEEE, pp. 518-523, 2004. Google Scholar
  17. 17.
    Kullmann, O.: Lean-sets: Generalizations of minimal unsatisfiable clause-sets. Discrete Applied Mathematics 130, 209–249 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Chvatal, V., Szemeredi, T.: Many hard Examples for Resolution. Journal of the Association for Computing Machinery 35, 759–768 (1988)zbMATHMathSciNetGoogle Scholar
  19. 19.
    Urquhart, A.: Hard Examples for Resolution. Journal of ACM 34, 209–219 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Franco, J., Gelder, A.V.: A Perspective on Certain Polynomial Time Solvable Classes of Satisfiability. Discrete Applied Mathematics 125, 177–214 (2003)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Zhenyu Chen
    • 1
  • Decheng Ding
    • 1
  1. 1.Department of MathematicsNanjing UniversityChina

Personalised recommendations