2 SAT variants complexity class

Question

Question: Which of the following languages are in P? which in NP? other classes?

a. EXACTLY-2-CNF (every clause in the formula has 2 differenet literelas)- does there exist a satisfying assignment s.t. at most k variables are TRUE.

b. same language but this time in each clause one literal is negated and the other isn't.

c. SAT-2-NAE - every clause has exactly 2 literals, is there an NAE satisfying assignment to the formula

d. mono-SAT-2-NAE - every clause as exactly 2 literals, none of them negated and it has a satisfying assignment

Thoughts: We tried a lot of reductions from 2SAT and other problems and cannot really determine most of the questions. We'd like to know what is the effect of the "monotone" property on the satisfiability such formulae... We'd also like some hints on how to reduce to these problems.

Answer 1

b. is completely trivial - just set each variable to FALSE.


d. trivially reduces to c. ​ ​ ​ c. reduces to d. as follows:
For each double-negative clause, remove the negatives. ​ Replace each
single-negative clause with 2 clauses, each of which has one of the original clause's variables
and a new variable that's shared with the other of the 2 new clauses but otherwise unused.

That works because:
for 2-variable clauses, NAE is just ≠
for boolean variables, ​ ​ ​ x ​ NAE ​ not y ​ ​ ​ simplifies to ​ x = y
for boolean variables, [there exists a y such that ​ ​ ​ x ≠ y ​ and ​ y ≠ z ] ​ if and only if ​ x = z

By ​ ​ ​ variables <-> vertices ​ and ​ clauses <-> edges ​ , ​ ​ ​ c. is equivalent to bipartiteness.
Bipartiteness is logspace-complete. ​ (Thus, c. and d. are logspace-complete.)


By throwing in k extra variables to handle "at most" vs. "exactly", a. is in W[P].
By ​ ​ ​ vertices -> variables ​ and ​ edges -> clauses ​ , ​ ​ ​ vertex cover reduces to ​ a. .
(Thus, for unrestricted k, a. is NP-complete.) ​ However, a. is fixed-parameter tractable.

Proof:
By replacing each clause with k+1 copies of itself and then [for each variable, putting in a
clause whose literals are both the negation of that variable], a. reduces to Almost 2-SAT.
By part 2.1 of that paper, that paper handles the case of clauses whose 2 literals are the same.
Theorem 7 of that paper explicitly covers "possible repeated occurrences of clauses".

I have no clue regarding possible kernalizability of a. or
$\big[$the space requirements of algorithms for a. whose runtimes aren't ​ max$\hspace{-0.03 in}\big(\hspace{-0.04 in}$n^Ω(k),$\hspace{.02 in}$2^Ω(n)$\hspace{-0.03 in}\big)\big]$.