positive CNF is a conjunctive normal form formula, where all literals are positive, i.e. the unary connective ¬ does not exist in the formula.
negative CNF is a conjunctive normal form formula, where all literals are negative, i.e. the unary connective ¬ appears next to each literal.
My question is:
Given a CNF, which is a conjunction of positive CNF and negative CNF, what is the complexity of the problem to determine that this special case of CNF is satisfiable?
Does exist polynomial time and space algorithm to solve this problem?
EDIT: Another name for "positive CNF" is "fact CNF", where all clauses are fact and another name for "negative CNF" is "goal CNF", where all clauses are goal.
... clause with no negative literals is sometimes called a fact
... clause without a positive literal is sometimes called a goal clause
Quoted from: this wikipedia documentation