[en] 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.
Disciplines :
Computer science Mathematics
Author, co-author :
Boros, Endre
Crama, Yves ; Université de Liège - ULiège > HEC Liège : UER > Recherche opérationnelle et gestion de la production
Hammer, Peter L.
Language :
English
Title :
Polynomial-time inference of all valid implications for Horn and related formulae
Aspvall B. (1980) Recognizing disguised NR(1)-instances of the satisfiability problem. J. Algorithms 1:97-103.
Aspvall B., Plass M.F., Tarjan R.E. (1979) A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Information Processing Lett. 8:121-123.
Blake A. (1937) Canonical expressions in Boolean algebra. Ph.D. Disertation, University of Chicago, ILL; .
Brown F.M. (1968) The origin of the method of iterated consensus. IEEE Trans. Computers 100-117:802.
Chang C.L., Lee R.C. Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York; 1973.
.
Dowling W.F., Gallier J.H. (1984) Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Logic Programming 3:267-284.
Gallaire H., Minker J. Logic and Databases, Plenum Press, New York; 1978.
Hansen P. (1976) A cascade algorithm for the logical closure of a set of binary relations. Information Processing Lett. 5:50-55.
Hansen P., Jaumard B., Minoux M. (1986) A linear expected-time algorithm for deriving all logical conclusions implied by a set of Boolean inequalities. Math. Programming 34:223-231.
Hooker J.N. (1988) Generalized resolution and cutting planes. Ann. Oper. Res. 12:217-239.
Hooker J.N. (1988) A quantitative approach to logical inference. Decision Support Systems 4:45-69.
Itai A., Makowsky J.A. (1987) Unification as a complexity measure for logic programming. J. Logic Programming 4:105-117.
Jones N.D., Laaser W.T. (1976) Complete problems for deterministic polynomial time. Theoretical Computer Sci. 3:105-117.
Kowalski R.A. Logic for Problem Solving, Elsevier, New York; 1979.
Lewis H.R. (1978) Renaming a set of clauses as a Horn set. Journal of the ACM 25:134-135.
Minoux M. (1988) LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation. Information Processing Lett. 29:1-12.
Provan J.S., Ball M.O. (1988) Efficient recognition of matroid and 2-monotonic systems. Applications of Discrete Mathematics , R.D., Ringeisen, F.S., Roberts, SIAM, Philadelphia; 122-134.
Quine W.V. (1955) A way to simplify truth functions. The American Mathematical Monthly 62:627-631.
Quine W.V. (1959) On cores and prime implicants of truth functions. The American Mathematical Monthly 66:755-760.
Robinson J.A. (1965) A machine-oriented logic based on the resolution principle. Journal of the ACM 12:23-41.
.
.
Valiant L.G. (1979) The complexity of enumeration and reliability problems. SIAM Journal on Computing 8:410-421.
Wang J., Vande Vate J. (1990) Question-asking strategies for Horn clause systems. Ann. Math. Art. Intell. 1:359-370.
