Complexity of a satisfiability problem I would like the know the complexity of a specific satisfiability problem. I have a feeling it could be solved in polynomial time, but I am not sure about it. The problem is described below.
Given $n$ boolean variables $v_1, v_2, \dots, v_n$ and two types of clauses.

At most $n$ clauses of the form $v_a \to \neg v_i \land \neg v_j \land \dots$ where $v_a$ cannot be on both sides of the implication.
At most $n$ clauses of the form $v_a \lor v_b \lor \dots$ where any combination of variables is possible (but no negations!).

The goal is to satisfy all the clauses. I have a feeling this can be done using limited backtracking just like with 2SAT as described on Wikipedia https://en.wikipedia.org/wiki/2-satisfiability#Limited_backtracking.
This is NP-hard.
Here is a reduction from SAT.  Suppose you have a CNF formula $\varphi$ with variables $x_1,\dots,x_n$.  Add variables $x'_1,\dots,x'_n$ and clauses of the form $x_i \to \neg x'_i$ and $x_i \lor x'_i$.  For each clause in $\varphi$, we add a corresponding $\cdots \lor \cdots$ clause: e.g., if $x_i \lor \neg x_j \lor x_k$ is a clause in $\varphi$, then we add the clause $x_i \lor x'_j \lor x_k$.  Once you've added all these clauses, add up the total number of clauses; say you have at most $m$ of the first type of clause and at most $m$ of the second type of clause.  Now add unused variables $x_{n+1},\dots,x_m$.  The result is an instance of your problem with $m$ variables and at most $m$ clauses of each type.  Now $\varphi$ is satisfiable iff this instance is satisfiable.