On generalized Horn formulas and \(k\)-resolution
type: Item
instance of: scholarly article
title: On generalized Horn formulas and \(k\)-resolution
zbMATH Open document ID: 0786.03009
DOI: 10.1016/0304-3975(93)90331-M
author: Hans Kleine Büning
published in: Theoretical Computer Science
publication date: 1994-05-05T00:00:00Z
review text: Several approaches to extend the set of Horn formulas to classes of CNF formulas for which SAT problem is still polynomially solvable have already been made. The paper presents a series of results concerning the satisfiability problem for the classes of propositional formulas belonging to the hierarchy introduced by Gallo and Scutella in 1988. The satisfiability problem for the class of \(k\)-generalized Horn formulas \(H_ k\) is treated in the framework of bounded-unit preference strategy based on an appropriate generalization of the resolution principle referred here as \(k\)-resolution. The completeness and soundness property of \(k\)-resolution for the class \(H_ k\) is proved first (theorem 3.3). Next, in theorem 3.5, the author establishes the insufficiency of \((k- 1)\)-resolution in deciding the satisfiability for \(H_ k\). It is pointed out that, in general, it is necessary to apply the \((k+1)\)-resolution to obtain all derivable literals. In the final section of the paper some comments concerning LLRI and 2-resolution are formulated. It is proved that any LLRI-refutable formula is 2-refutable too, but 2-resolution is strictly more powerful than LLRI.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68T27
Mathematics Subject Classification ID: 03F03
zbMATH DE Number: 417321
zbMATH Keywords: refutation
zbMATH Keywords: Horn formulas
zbMATH Keywords: satisfiability
zbMATH Keywords: resolution
reviewed by: Luminita State
MaRDI profile type: Publication
cites work: An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
cites work: Recognizing disguised NR(1) instances of the satisfiability problem
cites work: The Unit Proof and the Input Proof in Theorem Proving
cites work: Linear-time algorithms for testing the satisfiability of propositional horn formulae
cites work: Polynomially solvable satisfiability problems
cites work: The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
full work available at URL: 0304-3975(93)90331-m
OpenAlex ID: W1504884225
description: scientific article; zbMATH DE number 417321