The Incremental Satisfiability Problem for a Two Conjunctive Normal Form
The Incremental Satisfiability Problem for a Two Conjunctive Normal Form
复制标题
DOI：
10.1016/j.entcs.2016.11.004
复制
发表时间：
2016-12-08
影响因子：
--
通讯作者：
Hernandez, Jose A.
中科院分区：
文献类型：
--
作者：
De Ita Luna, Guillermo;Raymundo Marcial-Romero, J.;Hernandez, Jose A.
我们提出了一种新的方法来回顾当K和都是合取范式（CF）时的K证明。我们将该方法扩展到求解增量可满足性问题（ISAT），并给出了ISAT可以在多项式时间内求解的不同情况。特别地，我们提出了一种2-ISAT算法。我们的最后一种算法允许我们建立2-ISAT时间复杂度的上界，以及建立2-ISAT问题的一些可处理的情况。
We propose a novel method to review K proves phi when K and phi are both in Conjunctive Normal Forms (CF). We extend our method to solve the incremental satisfiablity problem (ISAT), and we present different cases where ISAT can be solved in polynomial time.Especially, we present an algorithm for 2-ISAT. Our last algorithm allow us to establish an upper bound for the time-complexity of 2-ISAT, as well as to establish some tractable cases for the 2-ISAT problem.