SOLVING THE INCREMENTAL SATISFIABILITY PROBLEM

被引：52

作者：

HOOKER, JN ^{[1
]}

机构：

[1] CARNEGIE MELLON UNIV, GRAD SCH IND ADM, PITTSBURGH, PA 15213 USA

来源：

JOURNAL OF LOGIC PROGRAMMING | 1993年 / 15卷 / 1-2期

关键词：

D O I：

10.1016/0743-1066(93)90018-C

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：177 / 186

页数：10

共 13 条

[1] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY
DAVIS, M
PUTNAM, H
[J]. JOURNAL OF THE ACM, 1960, 7 (03) : 201 - 215
[2] Hooker J. N., 1988, Decision Support Systems, V4, P45, DOI 10.1016/0167-9236(88)90097-8
[3] HOOKER JN, 1990, ANN MATH ARTIF INTEL, V1, P123
[4] Loveland D.W., 1978, AUTOMATED THEOREM PR, DOI DOI 10.1016/0378-4754(80)90081-6
[5] Quine W.V., 2018, AM MATH MON, V59, P521, DOI DOI 10.1080/00029890.1952.119881831
[6] Quine W. V., 1955, AM MATH MON, V62, P627, DOI [DOI 10.1080/00029890.1955.11988710, 10.1080/00029890.1955.11988710]
[7] [No title captured]
[8] [No title captured]
[9] [No title captured]
[10] [No title captured]

← 1 2 →