Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
type: Item
instance of: scholarly article
title: Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency.
zbMATH Open document ID: 1042.68105
DOI: 10.1016/S0020-0190(02)00267-3
author: Hans Kleine Büning
author: Xishun Zhao
published in: Information Processing Letters
publication date: 2003-01-21T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 03B05
zbMATH DE Number: 1856467
zbMATH Keywords: Propositional Logic
zbMATH Keywords: Minimal unsatisfiability
zbMATH Keywords: Formula homomorphism
zbMATH Keywords: Algorithms
MaRDI profile type: Publication
cites work: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
cites work: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
cites work: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
cites work: A perspective on certain polynomial-time solvable classes of satisfiability
cites work: On subclasses of minimal unsatisfiable formulas
cites work: Homomorphisms of conjunctive normal forms.
full work available at URL: s0020-0190(02)00267-3
OpenAlex ID: W2090627305
description: scientific article; zbMATH DE number 1856467