Abstract
The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,⋯,x n consist ofn +k clauses including it,x 1 V ⋯ Vx n and ⌉x 1 V ⋯ V ⌉x n It is shown that whenk ⩽4 the minimal unsatisfiability problem can be solved in polynomial time.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Papadimitriou, C. H., Wolfe, D., The complexity of facets resolved,Journal of Computer and System Sciences, 1988, 37: 2.
Papadimitriou, C. H., Yannakakis, M., The complexity of facets (and some facets of complexity),Journal of Computer and System Sciences, 1984, 28: 244.
Aspvall, B., Plass, M. F., Tarjan, R. E., A linear algorithm for testing the truth of certain quantified boolean formulas,Information Processing Letters, 1979, 8: 121.
Dowling, W. F., Gallier, J. H., Linear-time algorithm for testing the satisfiability of prepositional horn formulae,Journal of Logic Programming, 1984, 1: 267.
Davydov, G., Davydova, I., Solvable matrices,Mathematics of St. Petersburg University (in Russian), 1993, 1:3.
Franco, J., Pauli, M., Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem,Discrete Applied Mathematics, 1983, 5: 77.
Author information
Authors and Affiliations
Additional information
Project supported by the National Natural Science Foundation of China (Grant No. 19771045) and Nationl High-Tech R&D Project (863) (Grant No. 863-306-ET06-01-2).
Rights and permissions
About this article
Cite this article
Zhao, X., Ding, D. Two tractable subclasses of minimal unsatisfiable formulas. Sci. China Ser. A-Math. 42, 720–731 (1999). https://doi.org/10.1007/BF02878991
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02878991