# 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.

1. 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.
2. 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.

• I think this is not a research-level question because the answer can be found in wikipedia en.wikipedia.org/wiki/Boolean_satisfiability_problem. Dec 11 '20 at 19:47
• The "at most $n$" can be omitted (if you have too many clauses, pad with extra unused variables and then that constraint will be satisfied). I don't believe this is covered on Wikipedia; if you believe that, please provide more specifics.
– D.W.
Dec 11 '20 at 19:49
• Wikipedia mentions the NP-completeness of one-in-three positive 3-SAT, which is straightforward to reduce to this problem (with the observation that the limit for clauses doesn't really matter). Dec 11 '20 at 20:34

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.
• $x_i\to\neg x'_i$ and $x'_i\to\neg x_i$ are exactly the same clause ($\neg x_i\lor\neg x'_i$). There is no need to include it twice. Dec 11 '20 at 20:37