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.