Two tractable subclasses of minimal unsatisfiable formulas  

作　　者：赵希顺 丁德成 

出　　处：《Science China Mathematics》1999年第7期720-731,共12页中国科学：数学（英文版）

基　　金：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).

摘　　要：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₁,…, x_n consist of n+k clauses including _x₁V…V_{x_n} and （?） -（X₁）V…V（?）x_n. It is shown that when k≤4 the minimal unsatisfiability problem can be solved in polynomial time.

关 键 词：MINIMAL unsatisfiability SIMPLIFICATION PROCEDURE satisfaibility TEST SPLITTING collapsing. 

分 类 号：O224[理学—运筹学与控制论]