×

The complexity of variable minimal formulas. (English) Zbl 1196.68099

Summary: Based on the common properties of logic formulas: equivalence and satisfiability, the concept of variable minimal formulas with property preservation is introduced. A formula is variable minimal if the resulting sub-formulas with any variable omission will change the given property. Some theoretical results of two classes: variable minimal equivalence (VME) and variable minimal satisfiability (VMS) are studied. We prove that VME is NP-complete, and VMS is in \(D^{P}\) and coNP-hard.

MSC:

68Q25 Analysis of algorithms and problem complexity
03D15 Complexity of computation (including implicit computational complexity)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Zhang J. The Satisfiability of Logic Formulas -Methods, Tools and Applications (in Chinese). Beijing: Science Press, 2000
[2] Chen Z Y, Tao Z H, Xu B W, et al. Implication-based approximating bounded model checking. In: International Symposium on Fundamentals of Software Engineering, 2007, LNCS 4767: 350–363 · Zbl 1141.68459 · doi:10.1007/978-3-540-75698-9_23
[3] Li X W, Li G H, Shao M. Formal verification techniques based on Boolean satisfiability problem. J Comput Sci Technol, 2006, 20: 38–47 · Zbl 02241936 · doi:10.1007/s11390-005-0004-6
[4] Zhao X S. Complexity results on minimal unsatisfiable formulas–A survey. In: 9th Asian Logic Conference, 2005, 301–319
[5] Cook S A. The complexity of theorem-proving procedures. In: 3rd ACM Symposium on Theory of Computing, 1971, 151–158 · Zbl 0253.68020
[6] Papadimitriou C H, Wolfe D. The complexity of facets resolved. J Comput Syst Sci, 1988, 37: 2–13 · Zbl 0655.68041 · doi:10.1016/0022-0000(88)90042-6
[7] Zhao X S, Ding D C. Two tractable subclasses of minimal unsatisfiable formulas. Sci China Ser A, 1999, 29: 198–206 · Zbl 0937.03009
[8] Xu D Y. Applications of minimal unsatisfiable formulas to polynomially reduction for formulas. J Softw, 2006, 17: 1204–1212 · Zbl 1101.68848 · doi:10.1360/jos171204
[9] Shao M, Li G H, Li X W. Algorithms for extracting minimal unsatisfiable Boolean sub-formulas. J Comput-aid Design Comput Graphic, 2004, 16: 1542–1546
[10] Chen Z Y, Ding D C. Variable minimal unsatisfiability. In: Theory and Applications of Models of Computation, 2006, LNCS 3959: 262–273 · Zbl 1178.68536 · doi:10.1007/11750321_25
[11] Chen Z Y, Tao Z H, Kleine B H, et al. Applying variable minimal unsatisfiability in model checking. J Softw, 2008, 19: 39–47 · doi:10.3724/SP.J.1001.2008.00039
[12] Lau M F, Yu Y T. An extended fault class hierarchy for specification-based testing. ACM T Softw Eng Meth, 2005, 14: 247–276 · Zbl 05459518 · doi:10.1145/1072997.1072998
[13] Chen Z Y, Xu B W, Nie C H. A detectability analysis of fault classes for Boolean specifications. In: 23rd Annual ACM Symposium on Applied Computing, 2008. 390–394
[14] Shen S Y, Li S K. A fast counterexample minimization algorithm with refutation analysis and incremental SAT (in Chinese). J Softw, 2006, 17: 1034–1041 · Zbl 1101.68969 · doi:10.1360/jos171034
[15] Ravi K, Somenzi F. Minimal assignments for bounded model checking. In: 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2004. 31–45 · Zbl 1126.68486
[16] Papadimitriou C H, Yannakakis M. The complexity of facets (and some facets of complexity). J Comput Syst Sci, 1984, 28: 244–259 · Zbl 0571.68028 · doi:10.1016/0022-0000(84)90068-0
[17] Kleine B H, Lettmann T. Propositional Logic: Deduction and Algorithms. New York: Cambridge University Press, 1999 · Zbl 0957.03001
[18] Umans C. The minimum equivalent DNF problem and shortest implicants. J Comput Syst Sci, 2001, 53: 597–611 · Zbl 1006.68053 · doi:10.1006/jcss.2001.1775
[19] Chilenski J J, Miller S P. Applicability of modified condition/decision coverage to software testing. Softw Eng J, 1994, 9: 193–200 · doi:10.1049/sej.1994.0025
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.