,
Solving the Incremental Satisfiability Problem
Journal of Logic Programming, (1993)
Аннотация
Given a set of clauses in propositional logic that have been found satisfiable, we wish to check whether satisfiability is preserved when the clause set is incremented with a new clause. We describe an efficient implementation of the Davis-Putnam-Loveland algorithm for checking satisfiability of the original set. We then show how to modify the algorithm for efficient solution of the incremental problem, which is NP-complete. We also report computational results. Suppose that a given proposition does not follow from a knowledge base encoded in propositional logic. This can be checked by adding the proposition 's denial to the knowledge base and verifying that the resulting set of propositions is satisfiable. We wish to determine whether the proposition follows when the knowledge base is augmented by one or more new propositions. Rather than re-solve the satisfiability problem from scratch, we propose to use information gained while solving the original problem, so as to speed the solution of the new problem. We therefore address the incremental satisfiability problem of propositional logic: given that a set S of propositional clauses is satisfiable, check whether S fCg is satisfiable for a given clause C. Our investigation was occasioned by efforts to solve logic circuit verification problems 6, but it has application whenever one wishes to check again for logical inferences after enlarging a propositional knowledge base. It also plays a critical role in the solution of inference problems in first-order predicate logic 4, 7.
