Skip to main content
Article
Solving the Incremental Satisfiability Problem
The Journal of Logic Programming
  • John N. Hooker, Carnegie Mellon University
Date of Original Version
3-1-1992
Type
Article
Abstract or Description

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 the 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.

DOI
10.1016/0743-1066(93)90018-C
Citation Information
John N. Hooker. "Solving the Incremental Satisfiability Problem" The Journal of Logic Programming Vol. 15 Iss. 1-2 (1992) p. 177 - 186
Available at: http://works.bepress.com/jnhooker/37/