An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF

Authors
Davydov, G Davydova, I Buning, HK
Citation
G. Davydov et al., An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, ANN MATH A, 23(3-4), 1998, pp. 229-245
Citations number
6
Categorie Soggetti
Engineering Mathematics
Journal title
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE
ISSN journal
10122443 → ACNP
Volume
23
Issue
3-4
Year of publication
1998
Pages
229 - 245
Database
ISI
SICI code
1012-2443(1998)23:3-4<229:AEAFTM>2.0.ZU;2-Z
Abstract
We consider the minimal unsatisfiability problem for propositional formulas over n variables with n + k clauses for fixed k. We will show that in case of at most n clauses no formula is minimal unsatisfiable. For n + 1 clause s the minimal unsatisfiability problem is solvable in quadratic time. Furth er, we present a characterization of minimal unsatisfiable formulas with n + 1 clauses in terms of a certain form of matrices.