摘要
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.
The minimal unsatisfiability problem is considered of the propositional formulas in CNF which in the case of variables x<sub>1</sub>,…, x<sub>n</sub> consist of n+k clauses including <sub>x<sub>1</sub></sub>V…V<sub>x<sub>n</sub></sub> and （?） -（X<sub>1</sub>）V…V（?）x<sub>n</sub>. It is shown that when k≤4 the minimal unsatisfiability problem can be solved in polynomial time.
基金
Project supported by the National Natural Science Foundation of China (Grant No. 19771045)
Nationl High-Tech R&D Project (863) (Grant No. 863-306-ET06-01-2).
