On generalized Horn formulas and \(k\)-resolution (Q685363)

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.