Polynomial-time inference of all valid implications for Horn and related formulae
Polynomial-time inference of all valid implications for Horn and related formulae
复制标题
Horn 及相关公式的所有有效含义的多项式时间推理
DOI：
10.1007/bf01531068
复制
发表时间：
1990
影响因子：
1.2
通讯作者：
P. Hammer
中科院分区：
文献类型：
--
作者：
E. Boros;Y. Crama;P. Hammer
本文研究了一个一般推理问题的复杂性：给定一个合取范式的命题公式，求出该公式的所有素数蕴涵。这里，素数蕴涵是指最小子句，其有效性由公式的有效性隐含。我们证明，在一些合理的假设下，这个问题可以在输入的大小和质数蕴涵的数量上以多项式有界的时间来解决。在霍恩公式的情况下，结果专门产生一个算法，其复杂性仅与质数含义的数量线性增长。该结果也适用于推广霍恩公式和二次公式的一类公式。
This paper investigates the complexity of a general inference problem: given a propositional formula in conjunctive normal form, find all prime implications of the formula. Here, a prime implication means a minimal clause whose validity is implied by the validity of the formula. We show that, under some reasonable assumptions, this problem can be solved in time polynomially bounded in the size of the input and in the number of prime implications. In the case of Horn formulae, the result specializes to yield an algorithm whose complexity grows only linearly with the number of prime implications. The result also applies to a class of formulae generalizing both Horn and quadratic formulae.