Artículos de revistas
The Incremental Satisfiability Problem for a Two Conjunctive Normal Form
Autor
DE ITA LUNA, GUILLERMO; 57559
MARCIAL ROMERO, JOSE RAYMUNDO; 39478
HERNANDEZ SERVIN, JOSE ANTONIO; 89146
DE ITA LUNA, GUILLERMO
MARCIAL ROMERO, JOSE RAYMUNDO
HERNANDEZ SERVIN, JOSE ANTONIO
Institución
Resumen
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.