Given a propositional Horn formula, we show how to maintain on-line information about its satisfiability during the insertion of new clauses. A data structure is presented which answers each satisfiability question in O(1) time and inserts a new clause of length q in O(q) amortized time. This significantly outperforms previously known solutions of the same problem. This result is extended also to a particular class of non-Horn formulae already considered in the literature, for which the space bound is improved. Other operations are considered, such as testing whether a given hypothesis is consistent with a satisfying interpretation of the given formula and determining a truth assignment which satisfies a given formula. The on-line time and space complexity of these operations is also analyzed.

On-line algorithms for polynomially solvable satisfiability problems / Ausiello, G; Italiano, G. - In: JOURNAL OF LOGIC PROGRAMMING. - ISSN 0743-1066. - 10:1(1991), pp. 69-90. [10.1016/0743-1066(91)90006-B]

On-line algorithms for polynomially solvable satisfiability problems

Italiano G
1991

Abstract

Given a propositional Horn formula, we show how to maintain on-line information about its satisfiability during the insertion of new clauses. A data structure is presented which answers each satisfiability question in O(1) time and inserts a new clause of length q in O(q) amortized time. This significantly outperforms previously known solutions of the same problem. This result is extended also to a particular class of non-Horn formulae already considered in the literature, for which the space bound is improved. Other operations are considered, such as testing whether a given hypothesis is consistent with a satisfying interpretation of the given formula and determining a truth assignment which satisfies a given formula. The on-line time and space complexity of these operations is also analyzed.
On-line algorithms for polynomially solvable satisfiability problems / Ausiello, G; Italiano, G. - In: JOURNAL OF LOGIC PROGRAMMING. - ISSN 0743-1066. - 10:1(1991), pp. 69-90. [10.1016/0743-1066(91)90006-B]
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11385/191466
Citazioni
  • Scopus 30
  • ???jsp.display-item.citation.isi??? 23
social impact