The Incremental Satisfiability Problem for a Two Conjunctive Normal Form

2Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.

Abstract

We propose a novel method to review K⊢ϕ when K and ϕ 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.

Cite

CITATION STYLE

APA

De Ita Luna, G., Marcial-Romero, J. R., & Hernández, J. A. (2016). The Incremental Satisfiability Problem for a Two Conjunctive Normal Form. Electronic Notes in Theoretical Computer Science, 328, 31–45. https://doi.org/10.1016/j.entcs.2016.11.004

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free