Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency

详细信息    查看全文

• 作者：Kleine Bü ; ning ; Hans ; Zhao ; Xishun
• 关键词：Propositional Logic ; Minimal unsatisfiability ; Formula homomorphism ; Algorithms
• 刊名：Information Processing Letters
• 出版年：2002
• 出版时间：November 15, 2002
• 年：2002
• 卷：84
• 期：3
• 页码：147-151
• 全文大小：71.8 K

文摘

We say a propositional formula F in conjunctive normal form is represented by a formula H and a homomorphism φ, if φ(H)=F. A homomorphism is a mapping consisting of a renaming and an identification of literals. The deficiency of a formula is the difference between the number of clauses and the number of variables. We show that for fixed k≥1 and t≥1 each minimal unsatisfiable formula with deficiency k can be represented by a formula H with deficiency t and a homomorphism and such a representation can be computed in polynomial time.