Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. (Q1853126): Difference between revisions
From MaRDI portal
Removed claim: author (P16): Item:Q162005 |
Changed an Item |
||
Property / author | |||
Property / author: Zhao, Xishun / rank | |||
Normal rank |
Revision as of 20:15, 9 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. |
scientific article |
Statements
Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency. (English)
0 references
21 January 2003
0 references
We say a propositional formula \(F\) in conjunctive normal form is represented by a formula \(H\) and a homomorphism \(\phi\), if \(\phi(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\geqslant1\) and \(t\geqslant1\) 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.
0 references
Propositional Logic
0 references
Minimal unsatisfiability
0 references
Formula homomorphism
0 references
Algorithms
0 references