The Incremental Satisfiability Problem for a Two Conjunctive Normal Form

descriptionPublicationkeyboard_double_arrow_right Article , Conference object 01 Dec 2016 English Publisher:Elsevier BVJournal:Electronic Notes in Theoretical Computer Science, volume 328, pages 31-45 (issn: 1571-0661,

Copyright policy )

Authors: Guillermo De Ita Luna; José Raymundo Marcial-Romero; José Antonio Hernández Servín;

doi: 10.1016/j.entcs.2016.11.004

The Incremental Satisfiability Problem for a Two Conjunctive Normal Form

- Summary
- Subjects
- Metrics

Abstract

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.

Related Organizations

Benemérita Universidad Autónoma de Puebla
Mexico
Universidad Autónoma del Estado de México
Mexico
Facultad de Ingenieria
Argentina

Keywords

Theoretical Computer Science, Computer Science(all)

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	2
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average