International Journal of Computer Theory and Engineering

Abstract—Let K be a two conjunctive normal form and φ a three conjunctive normal form, both formulas are defined over the same set of variables. It is well known that SAT(K) is in the complexity class P, while SAT(φ) is a classic NP-Complete problem. We consider the computational complexity of determining SAT(Kφ) as an incremental satisfiability problem (2-ISAT). We show that this problem is NP-complete even if the number of occurrences of each variable in φ is one. Also, we propose a method to review SAT(Kφ). Our proposal is adequate to solve 2-ISAT problem. Our algorithm allows us to recognize tractable instances of 2-ISAT.

Index Terms—3-Coloring, incremental satisfiability roblem, 2-ISAT, NP-Complete problem, SAT problem.,

Cristina, López R. is with the Faculty of Computer Sciences in Benemérita Universidad Autónoma de Puebla, Puebla, México (mail: cristyna2001@hotmail.com).
Guillermo, De Ita. L. is with Faculty of Computer Sciences in Benemérita Universidad Autónoma de Puebla (e-mail: deita@ccc.inaoep.mx).
Pedro. Bello L. is with Faculty of Computer Sciences in Benemérita Universidad Autónoma de Puebla, Puebla, México (mail: pb5pbello@gmail.com).

[PDF]

Cite:Cristina López R., Guillermo De Ita L., and Pedro Bello L., "A Note for the Two Incremental Satisfiability Problem," International Journal of Computer Theory and Engineering vol. 9, no. 6, pp. 412-416, 2017.